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

Résumé : 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_Σ.
Type de document :
Thèse
Langage de programmation [cs.PL]. École polytechnique, 2015. Français
Liste complète des métadonnées

Littérature citée [69 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01197380
Contributeur : Bruno Bernardo <>
Soumis le : vendredi 11 septembre 2015 - 15:42:14
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Fichier

Licence


Copyright (Tous droits réservés)

Identifiants

  • HAL Id : tel-01197380, version 1

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〉

Partager

Métriques

Consultations de la notice

398

Téléchargements de fichiers

159