Definitions by Rewriting in the Calculus of Constructions

Abstract : The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prove the strong normalization of the reduction relation generated by the beta-rule and the user-defined rules under some general syntactic conditions including confluence. As examples, we show that two important systems satisfy these conditions: a sub-system of the Calculus of Inductive Constructions which is the basis of the proof assistant Coq, and the Natural Deduction Modulo a large class of equational theories.
Type de document :
Communication dans un congrès
16th Annual IEEE Symposium on Logic in Computer Science, Jun 2001, Boston, United States. 2001
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00105568
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 15:42:54
Dernière modification le : mardi 24 avril 2018 - 13:51:39
Document(s) archivé(s) le : mardi 6 avril 2010 - 17:53:16

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Definitions by Rewriting in the Calculus of Constructions. 16th Annual IEEE Symposium on Logic in Computer Science, Jun 2001, Boston, United States. 2001. 〈inria-00105568〉

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

82