I am a post-doctoral fellow in Computer Science at Inria Saclay in the Parisfal team of Dale Miller. Before that, I was a post-doc at McGill University, Canada, working with Brigitte Pientka, and in 2013-2014 at Aarhus University, Denmark, supervised by Olivier Danvy. Between 2009 and 2012, I was a Ph.D student at PPS, Université Paris Diderot and Università di Bologna. I worked also as an A.T.E.R at Université Paris Diderot for two years. During my thesis, I worked in the fields of type and proof theory, namely on proof certificates, incremental type-checking and sequent calculus. I am particularily interested in:
- the design of proof certificates, i.e., proof evidences that can be easily communicated and transmitted. They need to be compact and easily generated and checked.
- the interaction between functional programming and logical/specification frameworks, in particular those featuring HOAS encodings,
- the logical interpretation of functional language features, in particular program transformations (CPS, defunctionalization, deforestation),
- the implementation of theorem provers, both automated and interactive, in particular Coq and Beluga.
- Talk at the Type Theory and Realizability Working Group, PPS, Paris Diderot, and for the Parsifal team, LIX, École Polytechnique, with Brigitte Pientka: A Contextual Account of Staged Computations (October 2014, slides)
- Talk at the Complogic seminar, McGill University: Engineering CPS transformations (August 2014, slides)
- Article accepted for the TYPES 2014 post-proceedings: Typeful Normalization by Evaluation with Olivier Danvy and Chantal Keller (February 2014, PDF, accompanying code)
- Talk at the State Key Laboratory in Computer Science, ISCAS, Beijing: Proofs, upside down (December 2013, PDF)
Theory and Realizability Working Group, PPS, Paris Diderot,
with Olivier Danvy
Constructing normalization by evaluation with GADTs: a
(October 2013, abstract)
I propose a live-coding session, intended as an informal exposition of normalization by evaluation, using the OCaml type system's new feature: GADTs. I will show how it can be used to gradually turn the usual implementation of NbE "back" into an efficient normalization theorem for the simply-typed lambda-calculus, "proved in OCaml". I will then show how this method is modular: - knowing only the structure of types, we can normalize languages with i.e. control operators, thanks to CPS evaluation, - orthogonally, we can abstract from the representation of values (WIP) Its content is ongoing work together with Olivier Danvy and Chantal Keller.
- Article accepted at APLAS 2013: Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus, (PDF, slides (PDF), September 2013)
- Talk at DANSAS 2013, Odense, Denmark: From Natural Deduction to the Sequent Calculus by Passing an Accumulator (slides, August 2013)
- My Ph.D thesis is out! It is called Certificates for incremental type checking, and was defended at the university of Bologna on April 8, 2013. Find the manuscript here (PDF), along with the defense slides (PDF) (April 2013)
- Talk at the Workshop on Formal Meta-Theory, LIX, Ecole Polytechnique: Gasp: an OCaml library for manipulating LF objects (March 2013, slides)
- Talk at the Journées PPS, Trouville: From Natural Deduction to Sequent Calculus by reversing the λ-terms (September 2012, slides)
- Talk at the Type Theory and Realizability Working Group, PPS, Paris Diderot, with Yann Régis-Gianas: Certificates for incremental type checking (July 2012, slides)
- Draft: Certifying, incremental type checking with Yann Régis-Gianas (June 2012, PDF, accompanying code)
- Short paper accepted at TLDI 2012: Safe incremental type checking (January 2012, PDF)
- Talk at Gallium, with Yann Régis-Gianas (June 2011, slides)
- Talk at CEA LIST (LMeASI), with Yann Régis-Gianas (March 2011, slides)
- Talk at the Type Theory and Realizability Working Group, PPS, Paris Diderot, with Yann Régis-Gianas (January 2011, slides)
- Short paper accepted at MIPS 2010: Towards typed repositories of proofs, with Yann Régis-Gianas (PDF, slides)
- Ph.D thesis proposal: Towards formalized mathematics repositories based on type theory (PDF)
- Notes on Martin-Löf's Type Theory: De la Construction au Calcul (PDF, in french)
- Draft: Formal proof mining, a structure-oriented approach (PDF)
- Talk given in Bologna in 2008: Efficient and automatic recognition of mathematical structures in Coq (PDF)
- Master's thesis: Automatic recognition of mathematical structures in the proof assistant Coq (PDF, September 2008, in french)
- 2010-2011: IF1 - Informatique fondamentale L1, TP (page du cours)
- 2010-2011:SY5 - Systèmes L3, TD (page du cours)
- 2011-2012: IF1 - Informatique fondamentale L1, Cours/TD (page du cours)
- 2011-2012: PF1 - Principes de fonctionnement des machines binaires L1, TD (page du cours)
- 2011-2012: AC6 - Analyse syntaxique et compilation L3, TD/TP (page du cours)
- 2012-2013: OL3 - Outils logiques L2, TP (page du cours)
- 2012-2013: PF5 - Programmation fonctionnelle L3, TP (page du cours)
- 2012-2013: MV6 - Machines Virtuelles L3, Cours/TD (page du cours)
Here are the material for two lectures for COMP302 at McGill University in 2014:
- Lecture 3: More algebraic data types
- Lecture 4: Introduction to induction proofs and proof of programs.
I try to keep a public journal of my scientific activity, which takes the form of a blog, called Syntax!. You can find it here.
I initiated and contributed to various open-source projects. Most of the repositories can be found on my GitHub page. These include:
- I was a contributor of Coq early in my Ph.D.
- Gasp was the name of the prototype of incremental type checker I developed part of my Ph.D.
- During my stay at McGill, I contributed to Beluga.
- I recently got involved in embedded DSP programming. This project emerged.
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91120 Palaiseau, France