Termination Framework in Domain Theory

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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

Development

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:

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

Premodel

Model of the terminating fragment of ULC:

• Filters.v
• Interpretation.v
• Premodel.v
• RealizorPredicates.v
• Framework.v

Systems

Combinatory Logic: CL1.v

Simply Typed Lambda Calculus: STLC1.v

System F:

• Freevars.v
• F1.v

System T: T1.v