An implicit Calculus of Constructions with dependent sums and decidable type inference.
Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable.
Résumé
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.
Cette thèse propose un langage permettant de développer des programmes
certifiés purement calculatoires.
Pour cela deux systèmes de types sont présentés. Le premier, ICC_Σ,
est une extension du Calcul des Constructions Implicite de Miquel
(ICC), enrichi avec des sommes dépendantes. ICC_Σ est un système à la
Curry avec des opérateurs de type implicite. Ces opérateurs permettent
aux indications logiques de ne pas apparaître explicitement dans les
termes, rendant possible l'écriture de programmes certifiés purement
calculatoires. L'ajout des sommes dépendantes donne plus
d'expressivité au système et est un premier pas en vue de l'ajout des
types inductifs, déjà présents dans l'assistant de preuves Coq. Une
limitation de ICC_Σ est que l'inférence de type est vraisemblablement
indécidable.
Pour contourner ce problème, nous définisssons un deuxième système:
le Calcul des Constructions Implicite Annoté avec sommes dépendantes,
noté AICC_Σ. AICC_Σ est un système de types équivalent à ICC_Σ, mais
avec une syntaxe bicolore à la Church. Les indications logiques des
programmes apparaissent explicitement, rendant l'inférence de type
décidable, mais peuvent être marquées. AICC_Σ est muni d'un mécanisme
interne d'effacement qui transforme un terme de AICC_Σ avec
indications logiques en un terme de ICC_Σ purement calculatoire. Nous
prouvons que cet effacement est correct et complet, ce qui signifie
que les programmes valides de AICC_Σ correspondent exactement à ceux
de ICC_Σ.
Nous définissons également un algorithme d'inférence de type correct
et complet pour AICC_Σ. La combinaison de cet algorithme et du
mécanisme d'effacement rend possible la programmation certifiée dans
ICC_Σ.
Loading...