Jean-Marie Madiot

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
48 rue Barrault
CS 61534
75647 PARIS CEDEX
France

Office BJ27

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:

Higher-order languages: dualities and bisimulation enhancements

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

Stefania The Coqtail Project Gallais Gopi Kazoo 'tain ! Simon ??