Eliminating Dependent Pattern-Matching in Coq. Mangin, Cyprien, Master's Thesis,
Université Paris 7 Denis Diderot, August 2015.
If you want to intern at Inria with me on a general subject around Coq and type theory, you can just go ahead and contact me. I'm specifically looking for students interested in working on both theory and implementation.
- Cyprien Mangin, Master's internship on Equations and a SN proof of predicative system F , PhD started in 2015, co-advised with Bruno Barras
- Gaëtan Gilbert, PhD started in 2016, co-advised with Nicolas Tabareau
Ensembles nominaux dans Coq/SSreflect. Lewertowski, Gabriel, Master's Thesis,
Univeristé Paris Diderot Paris 7, September 2015.
Towards a Proof-Irrelevant Calculus of Inductive Constructions. Haselwarter, Philipp, Master's Thesis,
Université Paris 7, September 2014.