Arnaud Spiwack's PhD Thesis

Version & licenses
Creative Commons License

A Journey Exploring the Power and Limits of Dependent Type Theory

I defended my PhD thesis, titled Verified Computing in Homological Algebra: A Journey Exploring the Power and Limits of Dependent Type Theory on the 25-03-2011.

It had been carried out under the guidance of

  • Thierry Coquand
  • Benjamin Werner

It was reviewed by

  • Julio Rubio
  • Claudio Sacerdoti Coen

And was defended before a jury composed of

  • Yves Bertot (president)
  • André Hirschowitz
  • Paul-André Melliès
  • Julio Rubio
  • Claudio Sacerdoti Coen
  • Bas Spitters
  • Benjamin Werner

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.