ACADEMIA
In a previous life, I was 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 took a leave (disponibilité) from Cnam
at INA GRM. This page will
still be accessible but unmaintained.
Before that I was (in reverse chronological order):
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 (Cnam)
- 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)
- Sûreté de la programmation orientée objets (NFP101)
- Programmation réseau en Java
(INA136, SESF I3)
- Spécification
et Vérification de Programmes (UPMC, Master Info STL)
- Sûreté de la
programmation (USRS22, Master 1 SEMS, Cnam)
2017-2018 (Cnam)
2016-2017 (Cnam)
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:
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
Publications
-
Article accepted at JFLA 2017: Typeful Continuations (October
2016,
pdf, code)
-
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
-
VALS,
LRI, Deducteam,
LSV Cachan
and Gallium,
Inria: A Contextual Account of Staged
Computations (March
2016, slides)
-
Parsifal
team seminar, LIX, École Polytechnique, Two ways to the
focused sequent calculi (November
2015, slides)
-
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)
-
Complogic seminar, McGill University:
Engineering CPS transformations (August
2014, slides)
-
State
Key Laboratory in Computer
Science, ISCAS,
Beijing: Proofs, upside down (December
2013, PDF)
-
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)
-
DANSAS 2013,
Odense, Denmark: From Natural Deduction to the Sequent Calculus by Passing an Accumulator
(slides, August 2013)
-
Workshop
on Formal Meta-Theory, LIX, Ecole Polytechnique: Gasp: an OCaml library for manipulating LF objects
(March
2013, slides)
-
Journées
PPS, Trouville: From Natural Deduction to Sequent
Calculus by reversing the λ-terms (September
2012, slides)
-
Type
Theory and Realizability Working Group, PPS, Paris Diderot,
with Yann
Régis-Gianas: Certificates for incremental type checking
(July 2012, slides)
-
Gallium,
with Yann
Régis-Gianas (June
2011, slides)
-
CEA
LIST (LMeASI),
with Yann
Régis-Gianas (March
2011, slides)
-
Type
Theory and Realizability Working Group, PPS, Paris Diderot,
with Yann
Régis-Gianas (January
2011, slides)
-
Bologna, 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.