Definitions by rewriting in the Calculus of Constructions

Frédéric Blanqui 1, 2
Abstract : This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. On the one hand, the Calculus of Constructions is a powerful type system in which one can formalize the propositions and natural deduction proofs of higher-order logic. On the other hand, rewriting is a simple and powerful computation paradigm. The combination of both allows, among other things, to develop formal proofs with a reduced size and more automation compared with more traditional proof assistants. The main novelty is to consider a general form of rewriting at the predicate-level which generalizes the strong elimination of the Calculus of Inductive Constructions.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2005, 15 (1), pp.37-92. 〈10.1017/S0960129504004426〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00105648
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 11 octobre 2006 - 17:42:51
Dernière modification le : jeudi 10 mai 2018 - 02:07:00
Document(s) archivé(s) le : mardi 6 avril 2010 - 19:25:40

Fichiers

Identifiants

Collections

Citation

Frédéric Blanqui. Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2005, 15 (1), pp.37-92. 〈10.1017/S0960129504004426〉. 〈inria-00105648〉

Partager

Métriques

Consultations de la notice

392

Téléchargements de fichiers

90