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.
  • Pierre Giraud, PhD started in December 2020, on verified extraction to OCaml, co-advised with Nicolas Tabareau and Pierre-Marie Pédrot. Funded by a Nomadic Labs "CoqExtra" grant.

Past students:
  • Théo Winterhalter, who did his master's thesis on reflection and univalence [1] in 2017, started his PhD in September 2017, on universes and reflection, co-advised with Nicolas Tabareau at Inria Nantes. His thesis [2] on the "Formalisation and Meta-Theory of Type Theory" was defended in September 2020, now Théo is a post-doc at MPI in Bochum.
  • Gaëtan Gilbert, PhD started in September 2016, on proof-irrelevance and univalence, co-advised with Nicolas Tabareau at Inria Nantes. His thesis on "A type theory with definitional proof-irrelevance" was defended in December 2019. Gaëtan is now a research engineer in the Coq consortium.
  • Cyprien Mangin, Master's internship on Equations and a SN proof of predicative system F [3], 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 [4], co-advised with Nicolas Tabareau, Phd started in 2015, ended in 2016, now working at TrustInSoft.
  • Philipp Haselwarter, M2 internship on proof-irrelevance [5], 2014. Now with Andrej Bauer in Ljubljana.
A Restricted Version of Reflection Compatible with Univalent Homotopy Type Theory. Winterhalter, Théo, Master's Thesis, ENS Cachan, September 2017.
Formalisation and Meta-Theory of Type Theory. Winterhalter, Théo, PhD Thesis, Université de Nantes, 2020 - 2020NANT4012.
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!