Students and Postdocs
Current PhD students
Current interns
Ashish Kumar Barnawal (IIT Guwahati) on the Emacs and VSCode
interfaces
of Lambdapi .
Krishna Datta (Birla Institute of Technology and Science) on the
translation of STTfa to Agda.
Karthik
Viswanathan (IIIT-Hyderabad) on the development of a standard
library
for Lambdapi .
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
Guillaume Genestier
(Ecole Polytechnique ),
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
Amélie Ledein
(ENSIIE ) on the generation of
induction principles in dependent type theory.Tristan Delort (ENSIIE ) on
the translation of
Dedukti and STTfa to Agda .
François Lefoulon (ENSIIE )
on the development of the VSCode interface of Dedukti.
Gabriel Hondet
(ENAC )
on an efficient
implementation of rewriting , 2019.Houda Mouzoun (ENSEEIHT ),
M1 internship on developing a VSCode plugin for Lambdapi, 2019.
Jui-Hsuan Wu (ENS Paris ), M1
internship
on type-safety of
rewriting rules in dependent type theory and injectivity of
functions defined by rewriting rules , 2019.
Aristomenis-Dionysios Papadopoulos
(Imperial College ,
London), M1 internship on
the development of a
rewrite tactic in Dedukti , 2018.
Ismail Lachheb
(Sup Galilée ),
M1 internship on
the development of an
interface for interactive proof development with Lambdapi ,
2018. [slides] Guillaume Genestier
(Ecole Polytechnique ),
on the size-change
principle in type theory modulo rewriting , 2017.Rafaël Bocquet (ENS Paris ),
internship on Unification in type
theory modulo rewriting , 2017.
Antoine Defourné
(ENSIMAG ), master
thesis 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.
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 .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 .
