Sciweavers

RTA
2004
Springer

A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems

14 years 4 months ago
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems
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 β-reduction in the Calculus of Constructions.
Frédéric Blanqui
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where RTA
Authors Frédéric Blanqui
Comments (0)