The defense took place on the 30th of January 2014. For more information about the defense, see the defense page (the slides are available here). For more information about coercions, see my advisor webpage. For more information 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: