PhD
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
Abstract:
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.