Publication details

Saarland University Computer Science

Engineering Formal Systems in Constructive Type Theory

Steven Schäfer

PhD Thesis, Saarland University, 2019

This thesis presents a practical methodology for formalizing the meta-theory of formal systems with binders and coinductive relations in constructive type theory.
While constructive type theory offers support for reasoning about formal systems built out of inductive definitions, support for syntax with binders and coinductive relations is lacking. We provide this support.
We implement syntax with binders using well-scoped de Bruijn terms and parallel substitutions. We solve substitution lemmas automatically using the rewriting theory of theσ-calculus. We present the Autosubst library to automate our approach in the proof assistant Coq.
Our approach to coinductive relations is based on an inductive tower construction, which is a type-theoretic form of transfinite induction. The tower construction allows us to reduce coinduction to induction. This leads to a symmetric treatment of induction and coinduction and allows us to give a novel construction of the companion of a monotone function on a complete lattice.
We demonstrate our methods with a series of case studies. In particular, we present a proof of type preservation for CCω, a proof of weak and strong normalization for System F, a proof that systems of weakly guarded equations have unique solutions in CCS, and a compiler verification for a compiler from a non-deterministic language into a deterministic language.
All technical results in the thesis are formalized in Coq.

Project page (incl. all sources and further information)

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy