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.

• Download PDF for printing
• Download PDF for 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

• Abstract Reduction Systems
• Functional Extensionality
• Quotients

Chapter 3: De Bruijn Representation

• λ-Calculus Syntax
• Reduction and Substitutivity

Chapter 4: Subject Reduction in CC_ω

• Universes
• Syntax
• Reduction
• Church-Rosser Property
• Subtyping
• Typing
• Context Morphism Lemma
• Type Soundness and Subject Reduction

Chapter 5: Normalization in System F

• Polymorphic Types and Type Models
• Syntax of call-by-value System F
• Reduction in call-by-value System F
• Weak Normalization of call-by-value System F
• Syntax of System F
• Semantics of System F
• Strong Normalization of 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

Chapter 7: Strong Bisimilarity in CCS

• Syntax of CCS with recursive processes
• Semantics of CCS as a labelled transition system
• Congruence properties of open relative bisimilarity
• Properties of Strong Bisimilarity

Chapter 8: Axiomatic Semantics for Compiler Verification

• (Co-)directed (co-)induction
• Abstract axiomatic semantics
• Syntax of GC
• Semantics of GC
• Syntax of IC
• Semantics of IC
• Compiler from GC to IC

Legal notice, Privacy policy