IRILL - Research and Innovation on Free Software Annonce :
J'ai le plaisir de vous convier à ma soutenance de thèse, intitulée
"Vérification des résultats de l'inférence du compilateur OCaml"
Celle-ci aura lieu le mardi 23/10 à 15h15, dans les locaux de l'IRILL, sur le campus de Jussieu, 4 place Jussieu, Paris, 75005, en salle 101 tour 15, couloir 15-16 au premier étage.
Le jury est composé de :
Emmanuel CHAILLOUX (Prof. UPMC/Sorbonne Universités), rapporteur Jacques GARRIGUE (Prof. Nagoya University, Japon), rapporteur Sylvain CONCHON (Prof. Univ. Paris-Saclay), examinateur Catherine DUBOIS (Prof. ENSIIE), examinatrice Alain FRISCH (Société LEXIFI), examinateur Fabrice LE FESSANT (Société OCamlPro), co-directeur de thèse Michel MAUNY (DR Inria-Paris), co-directeur de thèse
La soutenance, après délibération du jury, sera suivie d'un pot auquel vous êtes également conviés.
======== Résumé :
OCaml est un langage fonctionnel statiquement typé, qui génère après inférence de types un arbre de syntaxe abstraite dans lequel chacun des noeuds est annoté avec un ensemble d’informations issues de cette inférence. Ces informations, en particulier les types inférés, constituent une preuve de typage de l’expression annotée. Ce manuscrit de thèse s’intéresse à la vérification de ces arbres annotés en les considérant comme des preuves de typages du programme, et décrit un ensemble de règles permettant d’en vérifier la cohérence. La formalisation de ces règles de vérification de preuves de types peut être vue comme une représensation du système de types du langage étudié. Cette thèse présente plusieurs aspects de la vérification d’arbres de syntaxe annotés. Le premier cas étudié est la formalisation d’un dérivé de MiniML où toutes les expressions sont annotées de manière théoriquement parfaite, et montre qu’il est possible d’écrire des règles de vérification de manière algorithmique, rendant directe la preuve de correction vis-à-vis de la spécification. La seconde partie s’intéresse à la formalisation de règles de vérification pour un sous-ensemble du premier langage intermédiaire d’OCaml, le TypedTree, accompagné d’un vérificateur implémentant ces règles. Ces règles constituent alors une représentation du système de types d’OCaml, document jusqu’alors inexistant, au mieux disséminé dans diverses publications.
========= Abstract:
OCaml is a statically typed programming language that generates typed annotated abstract syntax trees after type inference. Each of their nodes contains information derived from the inference like the inferred type and the environment used to find this information. These annotated trees can then be seen as typing proofs of the program. In this thesis, we introduce a consistency checking of type-annotated trees, considering them as typing proof, and we describe a set of rules that defines the consistency property. Such consistency checking rules can then be seen as a formalized representation of the type system, since consistency ensures the typing invariants of the language. This thesis introduces multiple aspects of checking type-annotated trees. First of all, it considers a simplified and ideal version of MiniML and formalizes a set of rules to check consistency. In this formalism, we consider ideally type-annotated trees, which might not be the case for OCaml typed trees. Such type checking rules are presented in an algorithmic form, reducing as much as possible the gap from formalism to implementation. As such, they ease the correction proof between the implementation of the type checker and the specification of the type system. The second part of this thesis is dedicated to the formalization of a set of rules for a subset of the OCaml annotated trees: the TypedTree. The formalism described in these chapters is implemented as a type checker working on large subset of the language, leaving the formalization of some aspects for a further work. These rules constitute a formalized representation of the OCaml type system in a single document.
A bientôt,
Pierrick Couderc