I am a PhD student in concurrency theory in the plume team (LIP, ENS Lyon) and the university of Bologna. I study the relations between process and functional calculi. My advisors are Daniel Hirschkoff and Davide Sangiorgi.
Email : jm (at) madiot (dot) org
COQTAIL
COQTAIL is a library of mathematical theorem proofs, mainly about analysis using the coq proof assistant.
Internship in Lyon
Internship 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.
Internship in Nijmegen
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.
Internship in Paris
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.
report - slides for CONCERTO - slides for COMPLICE
Internship in Marseille
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).
Quick links
