Students and Postdocs
Current PhD students
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
Gabriel Hondet
(ENAC ), PhD thesis 2019-2022
(grant Inria) on the translation of PVS proofs to Dedukti.Mohamed Yacine El
Haddad (Université
M'Hamed Bougarra Boumerdès ), PhD thesis 2018-2021 (grant
DigiCosme -LSV )
on integrating
automated theorem provers in proof assistants .Guillaume Genestier
(Ecole Polytechnique ),
now engineer 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é
Nice-Sophia-Antipolis ), 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
Quentin Buzet (L3 Télécom Paris) on developing a library on
arithmetic and lists in Lambdapi
Taïssir Marce (M1 University Paris-Saclay) on goal
transformation and proof (re)constructions
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 , now in postdoc at Virginia
Tech , 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.
Come back to main page .
