This is the formalisation of the master's thesis 
``Explicit convertibility proofs in Pure Type Systems'' 
written by Floris van Doorn and of the paper with the same name
written by Floris van Doorn, Herman Geuvers and Freek Wiedijk.

The formalisation is made with the Coq Proof Assistant, 
version 8.4pl1, using CoqIDE.

Coq and CoqIDE can be downloaded here: http://coq.inria.fr/

The formalisation and the thesis can be downloaded here:
http://www.cs.ru.nl/~freek/ptsf/

This formalisation was based on the formalisation of Vincent Siles.
The following files are new, all other files belong to Siles.

f_term.v 
f_env.v
f_typ.v 
f_typ2.v 
f_equivalence.v

For an (old) webpage of Siles, see 
http://www.lix.polytechnique.fr/~vsiles/

------------------------------------------------------------

Version of July 27, 2013.