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:
  • Antoine Allioux, PhD started in March 2018, on coherent algebraic structures in dependent type theory and homotopy type theory, co-advised with Yves Guiraud and Eric Finster.
  • Théo Winterhalter, who did his master's thesis on in 2017, started his PhD in September 2017, on universes and reflection, co-advised with Nicolas Tabareau at Inria Nantes.
  • Gaëtan Gilbert, PhD started in September 2016, on proof-irrelevance and univalence, co-advised with Nicolas Tabareau at Inria Nantes.

Past students:
  • Cyprien Mangin, Master's internship on Equations and a SN proof of predicative system F [1], PhD started in 2015 and ended in 2018, co-advised with Bruno Barras. Left for industry.
  • 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 TrustInSoft.
  • 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!