Lics

IEEE Symposium on Logic in Computer Science

Paper: Definitions by Rewriting in the Calculus of Constructions (at LICS 2001)

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 ß-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.

BibTeX

 @InProceedings{Blanqui-DefinitionsbyRewrit,
 author = 	 {Frédéric Blanqui},
 title = 	 {Definitions by Rewriting in the Calculus of Constructions},
 booktitle = {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
 year =	 {2001},
 month =	 {June}, 
 pages = {9--18},
 location = {Boston, MA, USA}, 
 publisher =	 {IEEE Computer Society Press}
 }