HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/inria-00105568
Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Wednesday, October 11, 2006 - 3:42:54 PM
Last modification on : Thursday, July 8, 2021 - 3:48:06 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 5:53:16 PM

Files

Identifiers

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. ⟨inria-00105568⟩

Share

Metrics

Record views

78

Files downloads

99