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

https://hal.inria.fr/inria-00100254
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, October 11, 2006 - 12:05:24 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM
Long-term archiving on: : Tuesday, April 6, 2010 - 1:12:32 AM

Files

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

252

Files downloads

163