We discuss and formalize a framework for proving termination of type theories, which has been developed by Bernadet and Lengrand following a technique introduced by Coquand. We then use the framework to formalize termination of Combinatory Logic, Simply Typed Lambda Calculus, System F, and System T. The Autosubst package is used to support reasoning about substitutions in terms and types.

Report: pdf

The code is available as a tar archive and online as a coqdoc html:

A resource aware type system with a reduction bound:

- Decidable.v
- Definitions.v
- TypeEquivalence.v
- Subsumption.v
- Contexts.v
- Types.v
- Weakening.v
- Substitution.v
- Reduction.v
- Termination.v

Model of the terminating fragment of ULC:

Combinatory Logic: CL1.v

Simply Typed Lambda Calculus: STLC1.v

System F:

System T: T1.v