A type-based termination criterion for dependently-typed higher-order rewrite systems. F. Blanqui. RTA'04. LNCS 3091, 15 pages. Full version.

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.

Statcounter W3C Validator Last updated on 26 November 2015. Come back to main page.