Paper Info
Title
Termination of rewriting in the Calculus of Constructions
Abstract
We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.
Year
DOI
Venue
2003
10.1017/S0956796802004641
Lecture Notes in Computer Science
Keywords
DocType
Volume
resulting system,important novelty,well-known higher order function,example dependent recursors,curry-howard isomorphism,function symbol,good candidate,proof assistant,strong normalization,higher order recursive path,calculus of constructions
Journal
13
Issue
ISSN
Citations 
2
0956-7968
21
PageRank 
References 
Authors
1.10
17
1
Name
Order
Citations
PageRank
Daria Walukiewicz-Chrząszcz1263.35