Students and Postdocs

Current PhD students

• Melanie Taprogge (Greifswald University, Germany), PhD thesis 2024-2027 in cotutelle with Alexander Steen (grant University Paris Saclay and Greifswald University) on the certification of automated theorem provers for higher-order logic.
• Ewen Broudin-Caradec (ENS Paris Saclay), PhD thesis 2025-2028 (grant ENS Paris Saclay) with Théo Winterhalter on phantom types in dependent type theory.
• Antoine Gontard (University Paris Cité), PhD thesis 2025-2028 (grant University Paris Saclay) on the translation of Isabelle to Rocq.
• Iván Martínez Comas (University Paris Cité), PhD thesis 2025-2028 (grant GS ISN) with Patrick Massot on the translation of HOL-Light and Rocq to Lean.
• Tiago Campos Ferreira (UFMG), PhD thesis 2026-2030 co-supervised by Haniel Barbosa (cotutelle between University Paris Saclay and Universidade Federal de Minas Gerais)

Past postdocs

• Michael Färber, postdoc 2019-2020 (grant Inria) on the translation of Isabelle proofs into Dedukti.
• Rehan Malak, postdoc 2019-2020 (grant DigiCosme) on the interactive handling of unification constraints and the formalization of models of cubical type theory in Dedukti.
• Rodolphe Lepigre, postdoc 2018-2019 (grant Inria) on the extension of Dedukti with metavariables and type inference.
• Franck Slama, postdoc 2018-2019 (grant Inria) on the development of Dedukti.

Past PhD students

• Rishikesh Vaishnav (University of California, San Diego), PhD thesis 2023-2026 on the translation between Lean and Dedukti.
• Thiago Felicissimo (Télécom Paris and UFMG, Brazil), PhD thesis 2021-2024 (grant University Paris-Saclay) on the translation of Agda proofs to Dedukti.
• Gabriel Hondet (ENAC), now at Alstom, PhD thesis 2019-2022 (grant Inria) on Expressing predicate subtyping in computational logical frameworks.
• Mohamed Yacine El Haddad (Université M'Hamed Bougarra Boumerdès), PhD thesis 2018-2021 (grant DigiCosme and LSV) on integrating automated theorem provers in proof assistants.
• Guillaume Genestier (Ecole Polytechnique), now at Tweag I/O, PhD thesis 2017-2020 (grant ENS Paris-Saclay) on Dependently-Typed Termination and Embedding of Extensional Universe-Polymorphic Type Theory using Rewriting.
• Kim-Quyen Ly, now engineer at Nomadic Labs, PhD thesis 2011-2014 on Automated verification of termination certificates.
• Cody Roux (Université Côte d'Azur), now software engineer at Draper Labs, PhD thesis 2008-2011 Terminaison à base de tailles: sémantique et généralisations (grant Inria).
• Pierre-Yves Strub (Université Paris-Diderot), now maître de conférence at Ecole Polytechnique, PhD thesis 2005-2008 (grant EADS Foundation) on type theory modulo decision procedures.
• Colin Riba (ENSIMAG), now maître de conférence at ENS Lyon, PhD thesis 2005-2007 (grant MESR) on Definitions by rewriting in the λ-calculus: confluence, reductibility and typing.

Past interns

• Antoine Gontard (University Paris Cité) on the development of tactics for automatically proving the equivalence of inductive type and function definitions between HOL-Light and Rocq, 2025.
• Amal Makni (M1 ENSTA) on the alignement of the definitions of real numbers in HOL-Light and Coq, 2024.
• Arunava Gantait (M1 Chennai Mathematical Institute) on the certification of PVS proofs, 2023.
• Nabin Kumar Sahoo (M1 Chennai Mathematical Institute) on the certification of Alethe proofs, 2023.
• Quentin Buzet (L3 Télécom Paris) on developing a library on arithmetic and lists in Lambdapi, 2022.
• Taïssir Marce (M1 University Paris-Saclay) on goal transformation and proof (re)constructions, 2022.
• Yann Leray (M1 ENS Paris) on Translating proofs between Isabelle and Dedukti, 2021.
• Thiago Felicissimo (M2 Télécom Paris and UFMG, Brazil) on Representing Agda and coinduction in the λΠ-calculus modulo rewriting, 2021.
• Aurélien Castre (L3 Télécom Paris) on the structuration of proof scripts in Lambdapi, 2021.
• Ashish Kumar Barnawal (L3, IIT Guwahati) on the Emacs and VSCode interfaces of Lambdapi, 2020.
• Amélie Ledein (M2, ENSIIE) on the generation of induction principles in dependent type theory, 2020.
• Tristan Delort (L3, ENSIIE) on the translation of Dedukti and STTfa to Agda, 2020.
• François Lefoulon (L3, ENSIIE) on the development of the VSCode interface of Dedukti, 2020.
• Gabriel Hondet (M2, ENAC) on an efficient implementation of rewriting, 2019.
• Houda Mouzoun (M1 ENSEEIHT) on developing a VSCode plugin for Lambdapi, 2019.
• Jui-Hsuan Wu (M1 ENS Paris), on type-safety of rewriting rules in dependent type theory and injectivity of functions defined by rewriting rules, 2019.
• Aristomenis-Dionysios Papadopoulos (M1 Imperial College, London) on the development of a rewrite tactic in Dedukti, 2018.
• Ismail Lachheb (M1 Sup Galilée) on the development of an interface for interactive proof development with Lambdapi, 2018. [slides]
• Guillaume Genestier (M2 Ecole Polytechnique) on the size-change principle in type theory modulo rewriting, 2017.
• Rafaël Bocquet (M1 ENS Paris), internship on Unification in type theory modulo rewriting, 2017.
• Antoine Defourné (M2 ENSIMAG) on Proof tactics in Dedukti, 2017.
• Rémi Nollet (ENS Lyon), internship Certification des fonctions générées par Moca, 2012.
• Frédéric Tuong, internship on the generation of processor simulators, 2011.
• Kim-Quyen Ly (Vietnam) on the certification of polynomial interpretations on rationals, 2010.
• Julien Bureaux (ENS Paris), now math teacher, internship on certifying the termination of Haskell programs, 2009. [slides]
• Antoine Taveneaux (ENS Lyon), internship Etude de bornes supérieures de complexité de programmes établies par typage, 2009. [slides]
• Sébastien Hinderer (Université Nancy I), now engineer at INRIA, master thesis Certification des preuves de terminaison par interprétations polynomiales, 2004.
• Pierre-Yves Strub (Université Paris-Diderot) on the integration of decision procedures in type theory, 2003.