Engineering Formal Systems in Constructive Type Theory
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.
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
Chapter 7: Strong Bisimilarity in CCS
Chapter 8: Axiomatic Semantics for Compiler Verification