Engineering Formal Systems in Constructive Type Theory
Draft
The latest draft is available in two versions. The submitted version has reduced colors for printing. The second version uses colored links for better on-screen viewing.
Coq Development
All results in the thesis are formalized in the Coq proof assistant. The full Coq development is available as an archive.
You can access the full documentation here, or by chapters below.
Chapter 2: Preliminaries
Chapter 3: De Bruijn Representation
Chapter 4: Subject Reduction in CCω
Chapter 5: Normalization in System F
Chapter 6: Tower-based Companions for Coinduction
- Tarski's Fixed Point theorem
- Correspondence between closure operators and inf-closed predicates
- Tower-based companion construction
- Parameterized tower induction
- Linearity of the tower construction
- The companion of a cocontinuous function
- The companion as a greatest fixed-point
- Example: companion of stream equality
- Example: companion of LTS similarity
- Example of a non-trivial L-Lattice