Matthias Puech

I am an associate professor (Maître de Conférence) in Computer Science at Cnam in the SyS team of the Cedric lab.

From September 2019 on I am on leave (disponibilité) from Cnam at INA GRM. This page will still be accessible but unmaintained.

Before that I was (in reverse chronological order):

post-doc at Inria Saclay in the Parisfal team of Dale Miller (2015-2016);
post-doc at McGill University, Canada, working with Brigitte Pientka (2014-2015);
post-doc at Aarhus University, Denmark, supervised by Olivier Danvy (2013-2014);
Ph.D. student and A.T.E.R at PPS, Université Paris Diderot and Università di Bologna. (2009-2012).

In the past, 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.

Teaching

2018-2019

Traitement du signal (intervention sur l'audio embarqué) (USRS09, STMN 1, Enjmin)
Synthèse de l'image et du son (STMN 2, ENJMIN)
Conception sonore (audio numérique) (US3334, Master 1 JMIN, Cnam ENJMIN)
Microcontrôleurs: architecture et communication (USRS26, Master 1 SEMS, Cnam)
Sûreté de la programmation orientée objets (NFP101)
Programmation réseau en Java (INA136, SESF I3)
Spécification et Vérification de Programmes (UPMC, Master Info STL)
Sûreté de la programmation (USRS22, Master 1 SEMS, Cnam)

2017-2018

Traitement du signal (intervention sur l'audio embarqué) (USRS09, STMN 1, Enjmin)
Sûreté de la programmation orientée objets (NFP101)
Microcontrôleurs: architecture et communication (USRS26, Master 1 SEMS, Cnam)
Synthèse de l'image et du son (STMN 2, ENJMIN)
Sûreté de la programmation (USRS22, Master 1 SEMS, Cnam)
Programmation réseau en Java (INA136, SESF I3)
Spécification et Vérification de Programmes (UPMC, Master Info STL)

2016-2017 (Cnam)

Sûreté de la programmation orientée objets (NFP101)
Intégration des systèmes client-serveur (NSY107)
Programmation Java : bibliothèques et patterns (NFA035)

2015-2016 (ESIEE)

I was a TA (chargé de TD) at ESIEE for René Natowicz, teaching introductory Algorithmics

2014 (McGill)

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.

2010-2013 (Paris Diderot)

During my A.T.E.R contract at Paris Diderot, I taught the following classes:

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)

Research

You will find below some of my work:

Publications

Article accepted at JFLA 2017: Typeful Continuations (October 2016, pdf, code)
Submitted draft: A Contextual Account of Staged Computations (March 2016, pdf)
Article accepted for the TYPES 2014 post-proceedings: Typeful Normalization by Evaluation with Olivier Danvy and Chantal Keller (February 2014, PDF, accompanying code)
Article accepted at APLAS 2013: Proofs, upside down: a functional correspondence between natural deduction and the sequent calculus, (PDF, slides (PDF), September 2013)
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)
Short paper accepted at MIPS 2010: Towards typed repositories of proofs, with Yann Régis-Gianas (PDF, slides)

Theses and technical reports

Ph.D. thesis: Certificates for incremental type checking, defended at the university of Bologna on April 8, 2013. Find the manuscript here (PDF), along with the defense slides (PDF) (April 2013)
Ph.D thesis proposal: Towards formalized mathematics repositories based on type theory (PDF, 2010)
Notes on Martin-Löf's Type Theory: De la Construction au Calcul (2009, PDF, in french)
Report: Formal proof mining, a structure-oriented approach (2009, PDF)
Master's thesis: Automatic recognition of mathematical structures in the proof assistant Coq (PDF, September 2008, in french)

Talks

Talk given at VALS, LRI, Deducteam, LSV Cachan and Gallium, Inria: A Contextual Account of Staged Computations (March 2016, slides)
Talk at the Parsifal team seminar, LIX, École Polytechnique, Two ways to the focused sequent calculi (November 2015, slides)
Talk at the Type Theory and Realizability Working Group, PPS, Paris Diderot, and for the Parsifal team, LIX, École Polytechnique, with Brigitte Pientka: From Staged Computations to Contextual Types (October 2014, slides)
Talk at the Complogic seminar, McGill University: Engineering CPS transformations (August 2014, slides)
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 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.
Talk at DANSAS 2013, Odense, Denmark: From Natural Deduction to the Sequent Calculus by Passing an Accumulator (slides, August 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)
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)
Talk given in Bologna in 2008: Efficient and automatic recognition of mathematical structures in Coq (PDF)

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 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 interesed in embedded DSP programming in C++ for music. Find my page for artistic/coding projects here

Contact

Mail: matthias.puech@lecnam.net

Physical address: Cnam
Bureau 33.1.18a
2 rue Conté
75003 Paris, France

PGP public key:

Cedric — Cnam — Equipe SyS