Sciences et Technologies de l'Information
Sommaire : Trois questions à Frédéric Blanqui, prix Specif | L'actualité de la semaine : | Dans les entreprises | Enseignement | Théories et concepts | La recherche en pratique | Manifestations | Le livre de la semaine | Détente |
"Je compte mener de front l'approfondissement théorique et les applications pratiques."
Asti-Hebdo : Votre thèse "Théorie des types et récriture" a été
primée par Specif. Elle va très loin dans l'abstraction de la logique et
de l'informatique théorique, et pourtant elle vise des objectifs pratiques et
mÍme industriels. Pouvez-vous nous préciser comment ?
Frédéric Blanqui : Mes recherches visent à améliorer les assistants à la démonstration utilisés dans la certification de programmes, de protocoles, etc. Pour prendre un exemple, significatif actuellement, les programmes Java enfouis dans les cartes à puce sont certifiés à l'aide d'assistants comme Coq, développé à l'Inria. D'autres chercheurs travaillent sur la certification de stimulateurs cardiaques, ou de systèmes de contrôle aérien à la Nasa.
Un tel travail de certification/preuve exige la formalisation de tout un environnement (sémantique des instructions. spécifications). Un outil comme Coq comporte donc à la fois un langage de programmation (en l'occurrence, comparable à ML), qui permet de définir des fonctions et de faire des calculs, un outil de description formelle des spécifications, et enfin le système d'aide à la démonstration qui permet d'établir la preuve à proprement parler à l'aide de tactiques semi-automatiques.
L'objectif de mon travail est de rendre ces systèmes d'aide à la démonstration plus souples et plus faciles à utiliser. L'idée maîtresse est de faciliter à l'utilisateur la définition des fonctions et des prédicats qu'il utilise. Dans un système comme Coq, les fonctions se définissent par récurrence. Ce mode d'expression n'est pas toujours très pratique. Il faut donc lui offrir un langage plus naturel et qui permette davantage d'automatisation. C'est le cas des langages à base de règles de réécriture. Ceux-ci ont aussi l'avantage de réduire la taille des preuves, qui peut devenir problématique dans certains cas.
Tout cela pose un certain nombre de problèmes théoriques et pratiques. Il faut en effet s'assurer de la cohérence logique d'un tel système, et aussi savoir si la correction des preuves faites par l'utilisateur peut Ítre effectivement vérifiée. D'o˜ l'aspect abstrait de ce travail passionnant.
Asti-Hebdo : Quel cheminement vous a conduit à ces questions ? Etes-vous au départ un logicien, un mathématicien, un informaticien ?
F.B. J'ai plutôt commencé par l'informatique, dans une optique pratique, puisque je suis entré à l' Ensimag. Je me suis ensuite intéressé à la logique, puis à l'informatique théorique. Mais, à vrai dire, les aspects théoriques m'ont toujours attiré. Dès mes études d'ingénieur, j'ai travaillé les mathématiques pures (à l'Institut Joseph Fourier de Grenoble).
C'est pourquoi, une fois obtenu mon diplôme d'ingénieur, après un séjour d'un an au Canada, je me suis lancé dans une thèse, à l'université d'Orsay, avec Jean-Pierre Jouannaud qui, à l'époque, dirigeait l'équipe Démons du LRI. Il est maintenant directeur du LIX, le laboratoire d'informatique de l'École polytechnique.
Cela m'a conduit à entrer en relations avec l'Inria, en particulier le projet Logical.
Asti-Hebdo : Comment allez-vous maintenant vous orienter ?
F.B. : Je vais poursuivre ma carrière de chercheur. Ma thèse apporte des solutions à un certain nombre de problèmes, mais il reste beaucoup de questions ouvertes et d'améliorations possibles.
Notez, par exemple, que les recherches sur la preuve de programmes se sont développées sur deux axes : vérification automatique et assistance à la démonstration. Actuellement, on observe une tendance à la coopération des deux communautés. En effet, d'une part, la vérification automatique a ses limites, qui appellent donc une intervention humaine. D'autre part les utilisateurs d'outils d'assistance sont demandeurs d'automatismes, quand ils sont possibles. Nous allons donc vers une intégration des deux types de systèmes.
Je compte mener de front l'approfondissement théorique et les applications pratiques. Je viens de faire un séjour post-doctoral à Cambridge (Royaume-Uni) sur la certification de protocoles cryptographiques. C'est dans ces perspectives que s'inscrit maintenant mon travail au LIX et ma collaboration à des projets comme Logical, de l'Inria. Vous trouverez plus de détails sur ma page web personnelle.