Jean-Marie Madiot

I am a postdoc in Princeton University; I work 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.

Submit to JFLA! Submit to ICE!


Formalizing 100 theorems: now 62% completed in Coq

Contact

Princeton University
Department of Computer Science
35 Olden Street
Princeton, NJ 08540-5233

jmadiot (at) cs (dot) princeton (dot) edu

Publications

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:

Higher-order languages: dualities and bisimulation enhancements

Teaching

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)

Quick links

The Coqtail Project Gallais Gopi Kazoo 'tain ! Simon ENS en grève ! Project Euler