KAHN GILLES (1946-2006)

Principaux travaux scientifiques

La première contribution marquante de Gilles Kahn a été la conception, en 1971, d'un modèle de calcul distribué asynchrone, aujourd’hui connu sous l’appellation « réseaux de Kahn ». Une version synchrone de ces réseaux est à la base de langages réactifs comme Lustre, dont le dérivé industriel SCADE (Safety Critical Application Development Environment) est utilisé massivement en aéronautique et dans les systèmes embarqués à haut degré de fiabilité. Gilles Kahn a été l'un des pionniers du domaine de la sémantique des langages de programmation, qui permet de donner un sens mathématique précis à un programme informatique. Dès 1975, il a organisé un congrès précurseur sur la vérification de programmes. Son équipe a contribué au succès du langage Ada, développé à la suite d’un appel d’offres du département de la Défense des États-Unis, en fournissant une sémantique formelle de la partie séquentielle du langage. Avec ses collègues de l'université d'Édimbourg, où il a passé l'année 1975, il a conçu une théorie des domaines de calcul concrets. Dans les années 1980, il a développé la notion de « sémantique naturelle » qui permet de manipuler un programme comme une formule et d’en calculer les propriétés. Cette percée a ouvert la voie au développement d'environnements de programmation comme Centaur, où les programmes sont manipulés de pair avec leur spécification. Convaincu de l'intérêt de la théorie des types alors en gestation (permettant d’aborder la conception des langages certifiés et des assistants de preuve), il organise en 1984 à Sophia-Antipolis l'International Symposium on Semantics of Data Types. Lors de ce congrès, qui inaugure un courant de recherche européen de pointe en certification de logiciel, a été présenté le premier article sur l’assistant de preuve Coq, au développement duquel il a contribué.