Chers collègues,
j'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée:
Typechecking in the λΠ-Calculus Modulo: Theory and PracticeLa soutenance aura lieu le vendredi 25 septembre à 15h dans les locaux de MINES ParisTech (60 Boulevard Saint-Michel, 75006 Paris) en salle V115.
Le jury sera composé de:
Vous êtes bien sûr également conviés au pot qui suivra.
En espérant vous y voir!
la vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d’énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu’un logiciel critique, c’est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. Dedukti est l’un de ces vérificateurs de preuves. Il implémente un système de type, le λΠ-Calcul Modulo, qui est une extension du λ-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, Dedukti implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs ce langage est particulièrement bien adapté à l’encodage d’autres système logiques. On peut, par exemples, importer dans Dedukti des théorèmes prouvés en utilisant d’autres outils tels que Coq, HOL ou encore Zenon, ouvrant ainsi la voie à l’interopérabilité entre tout ces systèmes.
Le λΠ-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l’unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par Dedukti. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc chercher à concevoir des critères garantissant la stabilité du typage par réduction et l’unicité des types qui soient décidables, de manière à pouvoir être implémentés par Dedukti.
Pour cela, nous donnons une nouvelle définition du λΠ-Calcul Modulo qui rend compte de l’aspect itératif de l’ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu’on peut ramener le problème de la stabilité du typage par réduction et de l’unicité des types à deux propriétés plus simples qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans Dedukti permettant d’augmenter grandement sa fiabilité.
automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. Dedukti is such a proof checker. It implements a type system, the λΠ-Calculus Modulo, that is an extension of the dependently typed λ-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, Dedukti implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in Dedukti theorems proved using other tools such as Coq, HOL or Zenon, initiating a form of interoperability between these systems.
The λΠ-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (that is stability of typing by reduction) and uniqueness of types, are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guarantying the coherence of the proof system, but also for proving the soundness and completeness of the type- checking algorithms implemented in Dedukti. Unfortunately, these properties are undecidable. In this thesis we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in Dedukti.
For this purpose, we give a new definition of the λΠ-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows us that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that are called product compatibility and well-typedness of rewrite rules. Hence, we study these two properties separately and we give effective sufficient conditions for them to hold. These ideas have been implemented in Dedukti allowing to increase its reliability.