I am a postdoctoral fellow in Computer Science at Inria Saclay in the Parisfal team of Dale Miller. Before that, I was a postdoc at McGill University, Canada, working with Brigitte Pientka, and in 20132014 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 typechecking 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.
Research
You will find below some of my work: 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 postproceedings: 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)

Talk at
the Type
Theory and Realizability Working Group, PPS, Paris Diderot,
with Olivier Danvy
and Chantal
Keller:
Constructing normalization by evaluation with GADTs: a
tutorial
(October 2013, abstract)
I propose a livecoding 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 simplytyped lambdacalculus, "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 MetaTheory, 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égisGianas: Certificates for incremental type checking (July 2012, slides)
 Draft: Certifying, incremental type checking with Yann RégisGianas (June 2012, PDF, accompanying code)
 Short paper accepted at TLDI 2012: Safe incremental type checking (January 2012, PDF)
 Talk at Gallium, with Yann RégisGianas (June 2011, slides)
 Talk at CEA LIST (LMeASI), with Yann RégisGianas (March 2011, slides)
 Talk at the Type Theory and Realizability Working Group, PPS, Paris Diderot, with Yann RégisGianas (January 2011, slides)
 Short paper accepted at MIPS 2010: Towards typed repositories of proofs, with Yann RégisGianas (PDF, slides)
 Ph.D thesis proposal: Towards formalized mathematics repositories based on type theory (PDF)
 Notes on MartinLöf's Type Theory: De la Construction au Calcul (PDF, in french)
 Draft: Formal proof mining, a structureoriented 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)
Teaching
During my A.T.E.R contract at Paris Diderot, I taught the following courses:
 20102011: IF1  Informatique fondamentale L1, TP (page du cours)
 20102011:SY5  Systèmes L3, TD (page du cours)
 20112012: IF1  Informatique fondamentale L1, Cours/TD (page du cours)
 20112012: PF1  Principes de fonctionnement des machines binaires L1, TD (page du cours)
 20112012: AC6  Analyse syntaxique et compilation L3, TD/TP (page du cours)
 20122013: OL3  Outils logiques L2, TP (page du cours)
 20122013: PF5  Programmation fonctionnelle L3, TP (page du cours)
 20122013: 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.
Blog
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.
Code
I initiated and contributed to various opensource 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.
Contact
Mail: puech@lix.polytechnique.fr
Physical address:
Inria Saclay
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91120 Palaiseau, France
Online: LinkedIn  Facebook  Twitter  Soundcloud  Youtube  Last.fm