Stage: Raisonnement et programmation fonctionnelle

Il s'agit de développement des outils qui construisent automatiquement des preuves sur les programmes fonctionnels.

Les systèmes de preuves basés sur la logique d'ordre supérieur fournissent un langage de programmation restreint où tous les programmes sont garantis de terminer. Il est possible d'utiliser ce langage de programmation pour écire des programmes répondant à des besoins pratiques, puis de démontrer que ces programmes effectuent les calculs attendus. Cette approche fournit donc une méthode pour construire des programmes sans erreur.

En pratique, les restrictions du langage de programmation fourni par le système de preuve limitent le pouvoir expressif et interdisent l'utilisation de cette méthode pour des projets ambitieux.

Lors d'un travail récent sur la vérification de correction d'un compilateur non trivial, nous avons détecté deux limitations pour lesquelles nous connaissons des méthodes d'encodage.

1. La programmation de haut niveau utilise des constructions de filtrage qui permettent au programmeur de décrire d'une part les différents schémas possibles pour les données que le programme doit considérer, et d'autre part la façon dont chaque procédure réagit sur ces schémas. Dans ces constructions filtrage, il est d'usage d'ordonner les règles de comportement et d'utiliser des règles par défaut.
2. En programmation fonctionnelle usuelle il est possible de définir des types de données récursifs qui contiennent des structures polymorphes.

L'usage dans les systèmes de démonstration est de ne considérer que les cas simples: les constructions de filtrage sont habituellement encodées en des constructions non ordonnées, au prix d'une multiplication des cas, et les types de données récursifs ne doivent contenir que des structures re-définies simultanément. Nous proposons de définir des outils de pré-traitement de définitions de structures de données et de programmes qui prennent mieux en compte les habitudes de programmation réelles.

Compétences requises

Les connaissances requises pour ce stage sont une bonne connaissance de la programmation en Ocaml et des aptitudes pour la vérification de démonstration sur ordinateur (principalement Coq)

Références

Le système Coq

Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, , Yves Bertot, Pierre Castéran, Springer, 2004.