Friday 18 September 2015, 10:00, INRIA Rocquencourt (23 avenue Italie 75013) room Orange: Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable, PhD defense of Bruno Bernardo.
Jury:
Abstract:
This thesis presents a programming language for developing purely computational certified programs.
We present two type systems. The first one, ICC_Σ, extends Miquel's Implicit Calculus of Constructions (ICC) with dependent sums. ICC_Σ is a Curry-style system with implicit type operators. With these operators, logical information may remain implicit, which makes it possible to write purely computational certified programs. Adding dependent sums gives more expressive power to the system and is a first step towards adding inductive types that are already built-in the Coq proof assistant. One drawback of ICC_Σ is that type inference is likely to be undecidable.
To solve that issue, we define a second system : the Annotated Implicit Calculus of Constructions, AICC_Σ. AICC_Σ is a type system equivalent to ICC_Σ but with a bicolor Church-style syntax. Logical information may appear explicitly, thus making type inference decidable. A built-in erasure procedure, that removes recursively the flagged parts, transforms an annotated AICC_Σ term into a purely computational ICC_Σ term. We prove that this procedure is correct and complete, which implies that valid AICC_Σ programs correspond exactly to valid ICC_Σ ones.
We also define a correct and complete type inference algorithm for AICC_Σ. This algorithm, combined with the erasure procedure makes certified programming in ICC_Σ possible.