en fr 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. Report as inadecuate




en fr 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. - Download this document for free, or read online. Document in PDF available to download.

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique Inria Paris-Rocquencourt 2 LIX - Laboratoire d-informatique de l-École polytechnique Palaiseau

Abstract : This thesis presents a programming language for developingpurely computational certified programs.We present two type systems. The first one, ICC Σ, extends Miquel-sImplicit Calculus of Constructions ICC with dependent sums. ICC Σ isa Curry-style system with implicit type operators. With theseoperators, logical information may remain implicit, which makes itpossible to write purely computational certified programs. Addingdependent sums gives more expressive power to the system and is afirst step towards adding inductive types that are already built-inthe Coq proof assistant. One drawback of ICC Σ is that type inferenceis likely to be undecidable. To solve that issue, we define a second system : the AnnotatedImplicit Calculus of Constructions, AICC Σ. AICC Σ is a type systemequivalent to ICC Σ but with a bicolor Church-style syntax. Logicalinformation may appear explicitly, thus making type inferencedecidable. A built-in erasure procedure, that removes recursively theflagged parts, transforms an annotated AICC Σ term into a purelycomputational ICC Σ term. We prove that this procedure is correct andcomplete, which implies that valid AICC Σ programs correspond exactlyto valid ICC Σ ones. We also define a correct and complete type inference algorithm forAICC Σ. This algorithm, combined with the erasure procedure makescertified programming in ICC Σ possible.

Résumé : Cette thèse propose un langage permettant de développer des programmescertifié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 MiquelICC, enrichi avec des sommes dépendantes. ICC Σ est un système à laCurry avec des opérateurs de type implicite. Ces opérateurs permettentaux indications logiques de ne pas apparaître explicitement dans lestermes, rendant possible l-écriture de programmes certifiés purementcalculatoires. L-ajout des sommes dépendantes donne plusd-expressivité au système et est un premier pas en vue de l-ajout destypes inductifs, déjà présents dans l-assistant de preuves Coq. Unelimitation de ICC Σ est que l-inférence de type est vraisemblablementindé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 Σ, maisavec une syntaxe bicolore à la Church. Les indications logiques desprogrammes apparaissent explicitement, rendant l-inférence de typedécidable, mais peuvent être marquées. AICC Σ est muni d-un mécanismeinterne d-effacement qui transforme un terme de AICC Σ avecindications logiques en un terme de ICC Σ purement calculatoire. Nousprouvons que cet effacement est correct et complet, ce qui signifieque les programmes valides de AICC Σ correspondent exactement à ceuxde ICC Σ. Nous définissons également un algorithme d-inférence de type correctet complet pour AICC Σ. La combinaison de cet algorithme et dumécanisme d-effacement rend possible la programmation certifiée dansICC Σ.

en fr

Keywords : certified programming implicit arguments Type theory type inference. dependent sums functional languages

Mots-clés : inférence de type. langages fonctionnels sommes dépendantes Théorie des types arguments implicites programmation certifiée





Author: Bruno Bernardo -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents