I defended my PhD thesis, titled Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory on the25-03-2011.
It had been carried out under the guidance of
It was reviewed by
And was defended before a jury composed of
You can read the memoir, but I also recorded the defence so that you could watch it (to abide with the host's policy, the video has been split in three parts, just follow the link at the end of each video to proceed to the next one). The slides are fairly legible on the video, provided you stream the hd version, however you may want to have them directly.
The sound recording is a bit bad so you might not hear all the questions asked by the jury. Also, I answer to some of the question in French, sorry about that.