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

`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

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

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:

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)

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.