My thesis is out!
by Matthias Puech
At last! The definitive, final and comprehensive version of my thesis manuscript is out. I defended it on April 8 in Bologna, Italy, and received both titles of “Dottore di ricerca” and “Docteur” in Computer Science, with great pride and relief. What an adventure! You can find my manuscript on my web page, precisely here; it’s called Certificates for incremental type-checking, and after much hesitation, I chose a blue cover for its printed version (it was a tough choice). It is already a little bit obsolete since I compulsively worked on that material even after its submission to avoid the baby blues, but I will nonetheless advertise it here, and eventually write about my advances in future posts. In short, if you are interested in proof certificates, manipulation of proof objects in a functional language, spine-form LF, incremental type-checking, contextual type theory, or the relationship between natural deduction and the sequent calculus, you might be interested in some parts of my manuscript.
In a little more details, the abstract printed on the (blue) back cover reads:
The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement; it is a central piece of compilers and proof assistants. First, we present a tool which supports the development of functional programs manipulating proof certificates (certifying programs). It uses LF as a representation metalanguage for higher-order proofs and OCaml as a programming language, and facilitates the automated and efficient verification of these certificates at run time. Technically, we introduce in particular the notion of function inverse allowing to abstract from a local environment when manipulating open terms. Then, we remark that the idea of a certifying type checker, generating a typing derivation, can be extended to realize an incremental type checker, working by reuse of typing subderivation. Such a type checker would make possible the structured and type-directed edition of proofs and programs. Finally, we showcase an original correspondence between natural deduction and the sequent calculus, through the transformation of the corresponding type checking functional programs: we show, using off-the-shelf program transformations, that the latter is the accumulator-passing version of the former.
Now that this is over with, I can go back to all the activities I’ve been missing so much these past months (years?); one of them is blogging. So stay tuned for some OCaml fun, serious proof theory and terrible hacks. You will hopefully read shortly about:
- the compilation of ML pattern-matching, explained as logically principled as I can,
- how you can write a gensym in OCaml without using the mutable keywords,
- handling syntax with binders in ML
- … and more!