I did my PhD thesis under the supervision of André Hirschowitz, from autumn 2008 until spring 2012.
PhD thesis
I defended my PhD thesis on May 23, 2012.
The manuscript was published in the Journal of Formalized Reasoning:
Initiality for Typed Syntax and Semantics
JFR Vol. 8, No 2 (2015), pp 1-155
doi:10.6092/issn.1972-5787/4712
It is also available as arXiv:1206.4556.
The committee consisted of
Coq code
In my PhD thesis I formalize the semantics of functional languages in a categorical setting in the Coq proof assistant. The goal is hence twofold:
- develop a library of category theory for general purpose
- use the library to prove some results about categorical syntax & semantics
The latest version of the library can be viewed here.
This site is compiled with
nanoc.
Built from code written by Cyril Cohen.
