My thesis was centered around the Russell language which provides facilities for writing dependently-typed programs in Coq. To further improve the usability of the system I also designed a typeclass system for Coq with Nicolas Oury and developed a new setoid rewriting tactic based on it. I also have a page recapitulting all the Coq stuff I did for my thesis or out of curiosity.
My defense took place on December 8th 2008 at 10.30am in room 79 of the LRI laboratory in Orsay (to get there). The committee was composed by:
Ms Véronique Benzaken, Professor at University of Paris-Sud 11 Mr Thierry Coquand, Professor at University of Göteborg Mr James McKinna, Professor at University of Nijmegen Ms Christine Paulin-Mohring, Professor at University of Paris-Sud 11 Mr François Pottier, Researcher at INRIA Rocquencourt Mr Philip Wadler, Professor at University of Edinburgh
Systems based on dependent type theory are getting considerable attention for the verification of computer programs as well as a practical tool for developing formal mathematical proofs involving complex and expensive computations. These systems still require considerable expertise from the users to be used efficiently. We design high-level constructs permitting to use languages based on dependent type theory as easily as modern functional programming languages, without sacrificing the powerful constructs of the former. We study a new language allowing to build certified programs while writing only their algorithmical squeleton and their specification. Typing in this system gives rise to proof obligations that can be handled interactively a posteriori. We demonstrate the main metatheoretical results on this system, whose proofs are partially mechanized, and present its implementation in the Coq proof assistant. Then we describe an integration and extension of the type classes concept à la Haskell into Coq, providing a simple interpretation of the constructs linked with type classes into the underlying dependent type theory. We demonstrate the usefulness of these dependent type classes for specifications and proofs and present an economical and powerful implementation of a generalized rewriting tactic based on them. We conclude by employing these contributions in the development of a certified library of a complex data structure called Finger Trees.An online version of the thesis is available (in french) along with the defense slides (in english) and some pictures.