Explicit Convertibility Proofs in Pure Type Systems

This is the Coq formalization of the of the master thesis by Floris van Doorn and the paper by Floris van Doorn, Herman Geuvers and Freek Wiedijk.

Download all files as zip.

Files: (in the html files, hover over a proof to see the Coq proof state)

These files require the formalization Equality is typable in any Pure Type Systems by Vincent Siles. These files are listed below.

back to main page