A New Elimination Rule for the Calculus of Inductive Constructions

Bruno Barras 1, 2 Pierre Corbineau 3 Benjamin Grégoire 4 Hugo Herbelin 2 Jorge Sacchini 4
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
4 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In Type Theory, definition by dependently-typed case analysis can be expressed by means of a set of equations — the semantic approach — or by an explicit pattern-matching construction — the syntactic approach. We aim at putting together the best of both approaches by extending the pattern-matching construction found in the Coq proof assistant in order to obtain the expressivity and flexibility of equation-based case analysis while remaining in a syntax-based setting, thus making dependently-typed programming more tractable in the Coq system. We provide a new rule that permits the omission of impossible cases, handles the propagation of inversion constraints, and allows to derive Streicher's K axiom. We show that subject reduction holds, and sketch a proof of relative consistency.
Type de document :
Communication dans un congrès
Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, 5497, pp.32-48, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_3〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00524938
Contributeur : Hugo Herbelin <>
Soumis le : vendredi 29 octobre 2010 - 11:03:47
Dernière modification le : mercredi 25 avril 2018 - 10:45:26
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 12:35:58

Fichier

types-BarCorGreHerSac08-dep-ma...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Sacchini. A New Elimination Rule for the Calculus of Inductive Constructions. Stefano Berardi and Ferruccio Damiani and Ugo de'Liguoro. Types for Proofs and Programs, Mar 2008, Torino, Italy. Springer, 5497, pp.32-48, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02444-3_3〉. 〈inria-00524938〉

Partager

Métriques

Consultations de la notice

563

Téléchargements de fichiers

137