Les travaux de recherche de l'équipe-projet GALLIUM portent sur la conception, la formalisation et l'implémentation de langages et systèmes de programmation. Notre objectif est d'améliorer la fiabilité (sûreté de fonctionnement et sécurité) des logiciels en utilisant :

• des langages de programmation de plus haut niveau, plus sûrs et plus expressifs, basés sur le paradigme de la programmation fonctionnelle ;
• la détection automatique d'erreurs de programmation à l'aide de systèmes de types et autres analyses statiques ;
• une meilleure intégration de la programmation et des méthodes formelles, en particulier la preuve sur machine de programmes.

• Systèmes de types, inférence de types et analyses statiques reliées.
  Le typage statique (la vérification d'un système de types pendant la compilation) est un outil très efficace pour détecter très tôt de nombreuses erreurs de programmation. De plus, les types aident à structurer non seulement les programmes eux-mêmes mais aussi les designs de langages de programmation. Parmi nos travaux en cours sur les systèmes de types, citons: le typage fin de structure de données, reflétant des invariants structurels à l'aide de types algébriques généralisés; l'inférence partielle de type pour des systèmes de types très expressifs, incluant du polymorphisme de première classe et d'ordre supérieur; et les systèmes de types pour les mécanismes de programmation à grande échelle (modules, classes, mixins, etc).

   

• Vérification formelle de compilateurs et autres outils de programmation.
  Lorsqu'on applique les méthodes formelles à un logiciel critique, comme exigé par les plus hauts niveaux de certification, il devient nécessaire de certifier formellement les outils qui servent à produire ce logiciel: compilateurs, analyseurs statiques, etc. Nous travaillons actuellement sur le développement et la vérification formelle, à l'aide de l'assistant de preuve Coq, d'un compilateur optimisant pour le langage C. La preuve Coq garantit que le code assembleur produit par ce compilateur a le même comportement sémantique que le programme source. Nous nous intéressons également aux spécifications et vérifications sur machine d'autres outils de programmation, comme les systèmes de types.

   

• Conception et implémentation de langages de programmation de haut niveau.
  Nous concevons et réalisons le langage Objective Caml et son environnement de programmation. Objective Caml est un langage de haut niveau, statiquement typé, qui combine les styles de programmation fonctionnel, impératif, à objets et modulaire. Nos réflexions actuelles autour de Caml et d'un éventuel successeur à ce langage comprennent l'étude de mécanismes unifiés pour la modularisation et la paramétrisation de fragments de code, ainsi que pour l'encapsulation et la délimitation des traits impératifs, ainsi que l'application de résultats récents en compilation et environnements d'exécution.

   

• Conception conjointe du logiciel et de sa preuve.
  La pratique des méthodes formelles dans l'industrie consiste à vérifier formellement du code déjà écrit, sans avoir le droit de le modifier. Nous défendons et utilisons une approche différente, où le code et ses preuves de correction sont développés en parallèle. Nous étudions divers moyens de faciliter cette approche de conception conjointe logiciel/preuve: enrichir les capacités de programmation de systèmes logiques tels que Coq; étendre des langages de programmation comme Caml avec des assertions logiques; et contribuer à des environnements unifiés pour la programmation et la preuve. Nous réalisons également le démonstrateur automatique Zenon, qui est une brique de base pour de tels environnements.

Logiciels

• Objective Caml

• ANR, action de recherche amont Compcert: compilation certifiée.
• Intel Corporation: implémentation du langage reFLect.
• Projet européen IST EDOS: environnement pour le développement et la distribution de logiciel libre.
• Membres industriels du Consortium Caml.