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

TL;DR

This paper introduces a new type-based termination criterion that effectively handles the combination of rewriting and beta-reduction in dependently-typed higher-order systems, extending previous criteria to more general settings.

Contribution

It extends existing type-based termination criteria to support general rewriting and dependent types in the Calculus of Constructions, enabling more powerful termination analysis.

Findings

Provides a new termination criterion for dependently-typed systems

Extends previous criteria to general rewriting and dependent types

Ensures termination in the combined rewriting and beta-reduction setting

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.