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

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

Contributor : Abes Star <>
Submitted on : Tuesday, April 16, 2019 - 10:56:24 AM
Last modification on : Tuesday, May 14, 2019 - 4:30:23 AM


Version validated by the jury (STAR)


  • HAL Id : tel-02100717, version 1


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⟩



Record views


Files downloads