I am a researcher at INRIA Paris, in the Gallium team -- now the Cambium team.
Before that, between August 2015 and December 2016, I was a postdoc in Princeton University; I worked with Andrew Appel in the Verified Software Toolchain project, focusing on verified reasoning on concurrent C programs.
Between March and August 2015, I was an invited researcher in Microsoft Research Cambridge, UK, working with Nick Benton on program logics.
I defended my PhD on concurrency theory on March 31st 2015 in Lyon, France.
Pop science talk about proofs and programs I gave at Institut Henri Poincaré for Maths en mouvements: "Des programmes sans bugs grâce aux mathématiques formelles ?"
Formalizing 100 theorems: as of November 2022, 79% completed in Coq
Contact
jean-marie.madiot (at) inria.fr
+33 1 80 49 41 89
Jean-Marie Madiot
INRIA Paris
2 rue Simone Iff
CS 42112
75589 Paris Cedex 12
France
Publications
A separation logic for heap space under garbage collection
(at POPL 2022)
with François Pottier
Modular coinduction up-to for higher-order languages via first-order transition systems (in LMCS, 2021)
with Damien Pous and Davide Sangiorgi
Name-passing calculi: from fusions to preorders and types
(in Information and Computation, 2016)
with Daniel Hirschkoff and Davide Sangiorgi
A behavioural
theory for a π-calculus with preorders
(in Journal
of Logical and Algebraic Methods in Programming,
2015)
with Daniel Hirschkoff and Xian Xu
A behavioural theory for a π-calculus with preorders
(at FSEN 2015, best paper award)
with Daniel Hirschkoff and Xian Xu
Symmetries and Dualities in Name-Passing Process Calculi
(in Computing with New Resources, 2014)
with Daniel Hirschkoff and Davide Sangiorgi
Bisimulations up-to: beyond first-order transition systems
(at CONCUR 2014)
with Damien Pous and Davide Sangiorgi
Name-passing calculi: from fusions to preorders and types
(at LICS 2013)
with Daniel Hirschkoff and Davide Sangiorgi
Duality and i/o-types in the π-calculus
(at CONCUR 2012)
with Daniel Hirschkoff and Davide Sangiorgi
PhD
I have a PhD in computer science from ENS Lyon and the University of Bologna, my advisors were Daniel Hirschkoff and Davide Sangiorgi. I conducted an investigation of types and duality in process calculi, and I provided bisimulation techniques for a variety of core higher-order languages (functional, imperative, and concurrent). Here is my dissertation:
Teaching
2023-2024: principles of programming languages (École Polytechnique, first-year students)
2023-2024: proofs of programs: separation logic (Université Paris Cité, MPRI, fifth-year students)
2022-2023: principles of programming languages (École Polytechnique, first-year students)
2022-2023: proofs of programs: separation logic (Université Paris Cité, MPRI, fifth-year students)
2022-2023: introduction à la programmation fonctionnelle (Université de Paris, third-year students)
2021-2022: introduction à l'informatique (École Polytechnique, first-year students)
2021-2022: proofs of programs: separation logic (Université Paris Cité, MPRI, fifth-year students)
2021-2022: introduction à la programmation fonctionnelle (Université de Paris, third-year students)
2020-2021: introduction à l'informatique (École Polytechnique, first-year students)
2020-2021: proofs of programs: separation logic (Paris 7, MPRI, fifth-year students)
2019-2020: introduction à l'informatique (École Polytechnique, first-year students)
2019-2020: proofs of programs: separation logic (Paris 7, MPRI, fifth-year students)
2018-2019: introduction à l'informatique (École Polytechnique, first-year students)
2018-2019: proofs of programs: separation logic (Paris 7, MPRI, fifth-year students)
2017-2018: principles of programming languages (École Polytechnique, first-year students)
2017-2018: proofs of programs: separation logic (Paris 7, MPRI, fifth-year students)
2014-2015: theory of programming (ENS Lyon, third-year students)
2014-2015: parallel algorithms and programs (ENS Lyon, fourth-year students)
2013-2014: computer-assisted proofs (ENS Lyon, fourth-year students)
2013-2014: algorithms and procedural programming (Université Claude Bernard Lyon 1, second-year students)
2012-2013: theory of programming (ENS Lyon, third-year students)
2012-2013: parallel algorithms and programs (ENS Lyon, fourth-year students)
Old projects
COQTAIL is a library of mathematical theorem proofs, mainly about analysis using the coq proof assistant. (See the github repository)
COQUILLE is a project of the first-year master students of the ENS Lyon, aiming to ease the use of coq to prove mathematical results.
Quick links
