Proof Engineering Presentations

Programming with dependent types: passing fad or useful tool?

An experience report on using / not using dependent types when programming and verifying functional programs in Coq.

Xavier Leroy, 2009

http://www.comlab.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf

Verifying a compiler: Why? How? How far?

Xavier Leroy, 2011

http://www.cgo.org/cgo2011/Xavier_Leroy.pdf