I did my PhD thesis under the supervision of André Hirschowitz, from autumn 2008 until spring 2012.
I defended my PhD thesis on May 23, 2012.The manuscript was published in the Journal of Formalized Reasoning:
It is also available as arXiv:1206.4556.
The committee consisted of
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.