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.

Formalizing 100 theorems: as of November 2022, 79% completed in Coq
JeanMarie Madiot
INRIA Paris
2 rue Simone Iff
CS 42112
75589 Paris Cedex 12
France
+33 1 80 49 41 89
jeanmarie.madiot (at) inria.fr
A separation logic for heap space under garbage collection
(at POPL 2022)
with François Pottier
Modular coinduction upto for higherorder languages via firstorder transition systems (in LMCS, 2020)
with Damien Pous and Davide Sangiorgi
Namepassing 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 NamePassing Process Calculi
(in Computing with New Resources, 2014)
with Daniel Hirschkoff and Davide Sangiorgi
Bisimulations upto: beyond firstorder transition systems
(at CONCUR 2014)
with Damien Pous and Davide Sangiorgi
Namepassing calculi: from fusions to preorders and types
(at LICS 2013)
with Daniel Hirschkoff and Davide Sangiorgi
Duality and i/otypes 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 higherorder languages (functional, imperative, and concurrent). Here is my dissertation:
20212022: separation logic (Université Paris Cité, MPRI, fifthyear students)
20212022: introduction à la programmation fonctionnelle (Université de Paris, thirdyear students)
20202021: introduction à l'informatique (École Polytechnique, firstyear students)
20202021: separation logic (Paris 7, MPRI, fifthyear students)
20192020: introduction à l'informatique (École Polytechnique, firstyear students)
20192020: separation logic (Paris 7, MPRI, fifthyear students)
20182019: introduction à l'informatique (École Polytechnique, firstyear students)
20182019: separation logic (Paris 7, MPRI, fifthyear students)
20172018: principle of programming languages (École Polytechnique, firstyear students)
20172018: separation logic (Paris 7, MPRI, fifthyear students)
20142015: theory of programming (ENS Lyon, thirdyear students)
20142015: parallel algorithms and programs (ENS Lyon, fourthyear students)
20132014: computerassisted proofs (ENS Lyon, fourthyear students)
20132014: algorithms and procedural programming (Université Claude Bernard Lyon 1, secondyear students)
20122013: theory of programming (ENS Lyon, thirdyear students)
20122013: parallel algorithms and programs (ENS Lyon, fourthyear 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 firstyear master students of the ENS Lyon, aiming to ease the use of coq to prove mathematical results.