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.

Current students:
  • Cyprien Mangin, Master's internship on Equations and a SN proof of predicative system F [1], PhD started in 2015, co-advised with Bruno Barras
  • Gaëtan Gilbert, PhD started in 2016, co-advised with Nicolas Tabareau

Past students:
  • Gabriel Lewertowski, Master's internship on Nominal Sets in Coq [2], co-advised with Nicolas Tabareau, Phd started in 2015, ended in 2016, now working at la Pitié-Salpetrière
  • Philipp Haselwarter, M2 internship on proof-irrelevance [3], 2014. Now with Andrej Bauer in Ljubljana.
Eliminating Dependent Pattern-Matching in Coq. Mangin, Cyprien, Master's Thesis, Université Paris 7 Denis Diderot, August 2015.
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.
Valid XHTML 1.1! Valid CSS!