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 in Lyon, France.

Formalizing 100 theorems: as of January 2020, 69% 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
Namepassing calculi: from fusions to preorders and types
(Information and Computation, 2016)
with Daniel Hirschkoff and Davide Sangiorgi
A behavioural
theory for a πcalculus with preorders
(Journal
of Logical and Algebraic Methods in Programming,
2015)
with Daniel Hirschkoff and Xian Xu
A behavioural theory for a πcalculus with preorders
(FSEN 2015, best paper award)
with Daniel Hirschkoff and Xian Xu
Symmetries and Dualities in NamePassing Process Calculi
(Computing with New Resources, 2014)
with Daniel Hirschkoff and Davide Sangiorgi
Bisimulations upto: beyond firstorder transition systems
(CONCUR 2014)
with Damien Pous and Davide Sangiorgi
Namepassing calculi: from fusions to preorders and types
(LICS 2013)
with Daniel Hirschkoff and Davide Sangiorgi
Duality and i/otypes in the πcalculus
(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:
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.
I spent five months in the Laboratoire de l'Informatique et du Parallélisme in the École Normale Supérieure de Lyon, under the supervision of Daniel Hirschkoff and Davide Sangiorgi. A new encoding of the lambdacalculus into the picalculus raised a question of duality inside the picalculus. In a first approach we use the picalculus with internal mobility, which has some notion of duality, and we extend its expressiveness. In a second approach we introduce a picalculus with a new operator and we study its duality. (See: report, presentation.)
Internship of two months at Radboud University, Nijmegen under the supervision of Freek Wiedijk. We attempt to build a formalisation of the specifications of imperative languages, like C, to reason about the semantics used in certified compilers. We focus on nondeterminism, undefined behaviors, or some less wellspecified aspects as stack handling. (See: report, presentation.)
Internship of three months at the Laboratoire d'Informatique de ParisNord, under the supervision of Damiano Mazza and Michele Pagani. Intersection types characterize a large set of lambdaterms (all the headnormalizable terms). They can be seen as coming from the multiplicative linear logic even if the latter is very restrictive. (See: report, slides for CONCERTO, slides for COMPLICE.)
Internship of two months at the laboratoire d'informatique fondamentale under the supervision of Rémi Eyraud. Contextual Binary Feature Grammars implies a formal langage defined thanks to a grammar. Unlike Chomsky grammars they take into account the context of a word to specify the corresponding derivation rule. The representation hopefully lets us extract a underlying semantic structure (the nonterminals of the grammar) of a formal language from a observable structure (the contexts). (See: report, presentation)