On type-based termination and dependent pattern matching in the calculus of inductive constructions

Jorge Sacchini 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Les assistants de preuve basés sur des théories des types dépendants sont de plus en plus utilisé comme un outil pour développer programmes certifiés. Un exemple réussi est l'assistant de preuves Coq, fondé sur le Calcul des Constructions Inductives (CCI). Coq est un langage de programmation fonctionnel dont un expressif système de type qui permet de préciser et de démontrer des propriétés des programmes dans une logique d'ordre supérieur. Motivé par le succès de Coq et le désir d'améliorer sa facilité d'utilisation, dans cette thèse nous étudions certaines limitations des implémentations actuelles de Coq et sa théorie sous-jacente, CCI. Nous proposons deux extension de CCI que partiellement resourdre ces limitations et que on peut utiliser pour des futures implémentations de Coq. Nous étudions le problème de la terminaison des fonctions récursives. En Coq, la terminaison des fonctions récursives assure la cohérence de la logique sous-jacente. Les techniques actuelles assurant la terminaison de fonctions récursives sont fondées sur des critères syntaxiques et leurs limitations apparaissent souvent dans la pratique. Nous proposons une extension de CCI en utilisant un mécanisme basé sur les type pour assurer la terminaison des fonctions récursives. Notre principale contribution est une preuve de la normalisation forte et la cohérence logique de cette extension. Nous étudions les définitions par filtrage dans le CCI. Avec des types dépendants, il est possible d'écrire des définitions par filtrage plus précises, par rapport à des langages de programmation fonctionnels Haskell et ML. Basé sur le succès des langages de programmation avec types dépendants, comme Epigram et Agda, nous développons une extension du CCI avec des fonctions similaires.
Type de document :
Thèse
Performance [cs.PF]. École Nationale Supérieure des Mines de Paris, 2011. English. <NNT : 2011ENMP0022>


https://pastel.archives-ouvertes.fr/pastel-00622429
Contributeur : Doriane Ibarra <>
Soumis le : lundi 12 septembre 2011 - 14:15:00
Dernière modification le : lundi 12 septembre 2011 - 15:18:17

Identifiants

  • HAL Id : pastel-00622429, version 1

Collections

Citation

Jorge Sacchini. On type-based termination and dependent pattern matching in the calculus of inductive constructions. Performance [cs.PF]. École Nationale Supérieure des Mines de Paris, 2011. English. <NNT : 2011ENMP0022>. <pastel-00622429>

Exporter

Partager

Métriques

Consultation de
la notice

477

Téléchargement du document

196