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

A type-based termination criterion for dependently-typed higher-order rewrite systems

Frédéric Blanqui 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the combination of rewriting and beta-reduction in the Calculus of Constructions.
Complete list of metadata

Contributor : Frédéric Blanqui Connect in order to contact the contributor
Submitted on : Wednesday, October 11, 2006 - 12:05:24 PM
Last modification on : Friday, February 4, 2022 - 3:31:18 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 1:12:32 AM





Frédéric Blanqui. A type-based termination criterion for dependently-typed higher-order rewrite systems. 15th International Conference on Rewriting Techniques and Applications - RTA'04, 2004, Aachen, Germany. ⟨inria-00100254⟩



Record views


Files downloads