Rishikesh Vaishnav (University of California, San Diego), PhD thesis 2023-2025 on the translation between Lean and Dedukti.
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.
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
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.
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.