I am a researcher at INRIA Paris, in the Gallium 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: now 62% completed in Coq

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

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

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:

2014-2015: separation logic (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.

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.)

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.)

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.)

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)