Skip to Main content Skip to Navigation
Theses

Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable.

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

Cited literature [69 references]  Display  Hide  Download

https://hal.inria.fr/tel-01197380
Contributor : Bruno Bernardo <>
Submitted on : Friday, September 11, 2015 - 3:42:14 PM
Last modification on : Thursday, March 5, 2020 - 6:30:54 PM

File

Licence


Copyright

Identifiers

  • HAL Id : tel-01197380, version 1

Collections

Citation

Bruno Bernardo. Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable.. Langage de programmation [cs.PL]. École polytechnique, 2015. Français. ⟨tel-01197380⟩

Share

Metrics

Record views

596

Files downloads

285