Sciences du logiciel

Présentation de la recherche

Pr Xavier Leroy

La recherche de la chaire Sciences de logiciel s'effectue dans le cadre de l'équipe-projet Cambium, commune entre le Collège de France et l'Inria.

Les travaux de l'équipe visent à améliorer la fiabilité, la sûreté et la sécurité du logiciel en faisant progresser les langages de programmation et les méthodes de vérification formelle de programmes. La conception, la formalisation et la mise en œuvre de langages de programmation jouent un rôle central dans les activités de l'équipe. Les principaux thèmes de recherche sont les systèmes de types et les algorithmes d'inférence de types, la vérification déductive de programmes, le parallélisme à mémoire partagée, et les modèles mémoires faiblement cohérents. L'équipe s'intéresse tout autant aux fondements théoriques qu'aux applications réalistes.

L'équipe Cambium conçoit et développe deux grands logiciels de recherche qui intègrent et font passer dans la pratique bon nombre de ses résultats :

  • OCaml, un langage de programmation fonctionnel statiquement typé et son implémentation. OCaml est, avec Haskell, un des deux langages fonctionnels typés les plus utilisés dans l'industrie comme dans la recherche ;
  • CompCert, un compilateur vérifié pour logiciels embarqués critiques. CompCert est le premier compilateur réaliste qui a été formellement vérifié à l'aide de méthodes formelles (l'assistant à la démonstration Coq).