Skip to Main content Skip to Navigation
Theses

Vérification des résultats de l'inférence de types du langage OCaml

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.
Document type :
Theses
Complete list of metadatas

Cited literature [74 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-02100717
Contributor : Abes Star :  Contact
Submitted on : Tuesday, April 16, 2019 - 10:56:24 AM
Last modification on : Monday, May 11, 2020 - 12:26:50 PM

File

66213_COUDERC_2018_archivage.p...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02100717, version 1

Citation

Pierrick Couderc. Vérification des résultats de l'inférence de types du langage OCaml. Informatique et langage [cs.CL]. Université Paris-Saclay, 2018. Français. ⟨NNT : 2018SACLY018⟩. ⟨tel-02100717⟩

Share

Metrics

Record views

206

Files downloads

138