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

Formalizing 100 theorems: as of January 2020, 69% completed in Coq!

Contact

Jean-Marie Madiot
INRIA Paris
2 rue Simone Iff
CS 42112
75589 Paris Cedex 12
France

+33 1 80 49 41 89

jean-marie.madiot (at) inria.fr

Publications

Name-passing 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 Name-Passing Process Calculi (Computing with New Resources, 2014)
with Daniel Hirschkoff and Davide Sangiorgi

Bisimulations up-to: beyond first-order transition systems (CONCUR 2014)
with Damien Pous and Davide Sangiorgi

Name-passing calculi: from fusions to preorders and types (LICS 2013)
with Daniel Hirschkoff and Davide Sangiorgi

Duality and i/o-types in the π-calculus (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

2019-2020: separation logic (Paris 7, MPRI, fifth-year students)

2018-2019: introduction à l'informatique (École Polytechnique, first-year students)

2018-2019: separation logic (Paris 7, MPRI, fifth-year students)

2017-2018: principle of programming languages (École Polytechnique, first-year students)

2017-2018: 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)

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.

Internships

Lyon

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 lambda-calculus into the pi-calculus raised a question of duality inside the pi-calculus. In a first approach we use the pi-calculus with internal mobility, which has some notion of duality, and we extend its expressiveness. In a second approach we introduce a pi-calculus with a new operator and we study its duality. (See: report, presentation.)

Nijmegen

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 non-determinism, undefined behaviors, or some less well-specified aspects as stack handling. (See: report, presentation.)

Paris

Internship of three months at the Laboratoire d'Informatique de Paris-Nord, under the supervision of Damiano Mazza and Michele Pagani. Intersection types characterize a large set of lambda-terms (all the head-normalizable 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.)

Marseille

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 non-terminals of the grammar) of a formal language from a observable structure (the contexts). (See: report, presentation)