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 3: De Bruijn Representation

Author: Steven Schäfer

Created: 2019-03-02 Sat 14:04