Version française

Jean-Marie Madiot

I am a PhD student in concurrency theory in the plume team (LIP, ENS Lyon) and the university of Bologna. My advisors are Daniel Hirschkoff and Davide Sangiorgi. This joint PhD between Lyon and Bologna is supported by Rhône-Alpes and Université Franco-Italienne.

jm (at) madiot (dot) org       +33 (0) 4 72 72 82 30


Duality and i/o-types in the π-calculus, with D. Hirschkoff and D. Sangiorgi, CONCUR 2012.

Name-passing calculi: from fusions to preorders and types, with D. Hirschkoff and D. Sangiorgi, LICS 2013.


I am a teaching assistant for the courses computer-assisted proofs in ENS Lyon and algorithms and procedural programming.

Last year it was for the courses theory of programming and parallel algorithms and programs.


COQTAIL is a library of mathematical theorem proofs, mainly about analysis using the coq proof assistant. (See the sourceforge 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.



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

Quick links

The Coqtail Project Gallais Gopi Kazoo Info reseau Project Euler For you, bot.