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.

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

Chapter 7: Strong Bisimilarity in CCS

Chapter 8: Axiomatic Semantics for Compiler Verification

Legal notice, Privacy policy