Termination Framework in Domain Theory

Saarland University Computer Science

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:

Target System

A resource aware type system with a reduction bound:


Model of the terminating fragment of ULC:


Combinatory Logic: CL1.v

Simply Typed Lambda Calculus: STLC1.v

System F:

System T: T1.v

Legal notice, Privacy policy