Certificates for incremental type checking
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement ; it is a central piece of compilers and proof assistants. First, we present a tool which supports the development of functional programs manipulating proof certificates (certifying programs). It uses LF as a representation metalanguage for higher-order proofs and OCaml as a programming language, and facilitates the automated and efficient verification of these certificates at run time. Technically, we introduce in particular the notion of function inverse allowing to abstract from a local environment when manipulating open terms. Then, we remark that the idea of a certifying type checker, generating a typing derivation, can be extended to realize an incremental type checker, working by reuse of typing subderivation. Such a type checker would make possible the structured and type-directed edition of proofs and programs. Finally, we showcase an original correspondence between natural deduction and the sequent calculus, through the transformation of the corresponding type checking functional programs : we show, using off-the-shelf program transformations, that the latter is the accumulator-passing version of the former.
Abstract FR:
La thématique centrale de cette thèse est l'étude des algorithmes de typage, du point de vue des langages de programmation comme du point de vue de la théorie de la preuve. Un algorithme de typage prend en entrée un programme ou une preuve, représenté comme un objet syntaxique, et vérifie sa validité vis-à-vis d'une spécification ou d'un énoncé ; c'est un élément central des compilateurs et des assistants à la preuve. Premièrement, nous présentons un outil d'assistance au développement de programmes fonctionnels manipulant des certificats de preuve (programmes certifiants). Il utilise LF comme métalangage de représentation d'ordre supérieur des preuves et OCaml comme langage de programmation, et facilite la vérification automatique et efficace de ces certificats à l'exécution. Techniquement, nous introduisons en particulier la notion de fonction inverse permettant de s'abstraire d'un environnement local quand on manipule des termes ouverts. Ensuite, nous remarquons que l'idée d'un vérificateur de type certifiant, qui génère une dérivation de typage, peut être étendue pour en faire un vérificateur de type incrémental, fonctionnant par réutilisation de sous-dérivations de typage. Un tel vérificateur de type rendrait possible l'édition structurée et dirigée par le type programmes et de preuves. Enfin, nous mettons en évidence une correspondance originale entre la déduction naturelle et le calcul des séquents, passant par la transformation des programmes fonctionnels de vérification de type correspondants : nous montrons en utilisant des transformations standard que le deuxième est la version par passage d'accumulateur du premier.