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 am specifically looking for students interested in working on both theory and implementation.

Current students:

• Yann Leray, PhD started in September 2023, after an internship on the formalization of SProp in 2022. Yann is working on the formal verification in MetaCoq and the integration in Coq of SProp and rewrite rules.

Past 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. Defended his thesis in July 2023, entitled Higher Structures in Homotopy Type Theory [1]. Left for industry.
• 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.
• Théo Winterhalter, who did his master's thesis on reflection and univalence [2] in 2017, started his PhD in September 2017, on universes and reflection, co-advised with Nicolas Tabareau at Inria Nantes. His thesis [3] 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 [4] was defended on 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 [5], 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 [6], co-advised with Nicolas Tabareau, Phd started in 2015, ended in 2016, now working at TrustInSoft.
• Philipp Haselwarter, M2 internship on proof-irrelevance [7], 2014. Now with Andrej Bauer in Ljubljana.