The defense took place on the 30th of January 2014. For more informations about the defense, see the defense page (the slides are available here). For more informations about coercions, see my advisor webpage. For more informatinos about my PhD, see my webpage.
The last version of the manuscript is the final version, but a printed version, prerelease version, and the version for review are also available:
The Coq development is available in three forms: