À partir de septembre 2011, je suis en thèse de concurrence sur les relations entre calculs de processus et fonctionnels avec Daniel Hirschkoff et Davide Sangiorgi. Je suis dans l'équipe plume (LIP, ENS Lyon) en cotutelle avec l'université de Bologne.
Email : jm (at) madiot (dot) org
Projet COQTAIL
COQTAIL est une bibliothèque de preuves de théorèmes, majoritairement d'analyse, dans le cadre du logiciel d'assistant de preuves coq. Ce projet est la suite de la partie preuves du projet COQUILLE.
Stage à Lyon
Stage au Laboratoire de l'Informatique et du Parallélisme à l'École Normale Supérieure de Lyon, sous la direction de Daniel Hirschkoff et Davide Sangiorgi. Un nouvel encodage du lambda-calcul dans le pi-calcul a posé une question de dualité dans des processus du pi-calcul. D'un côté on augmente la portée du pi-calcul à mobilité interne car ce dernier comprend une notion de dualité. D'un autre côté, on construit un sur-calcul du pi-calcul et on étudie la dualité dans celui-ci.
Stage à Nimègue
Stage au Laboratoire d'informatique de l'université de Radboud sous la direction de Freek Wiedijk. Il s'agit d'une approche voulue générale d'une formalisation en Coq de spécifications des langages de programmation impératifs, plus spécifiquement du C, en vue d'une validation des sémantiques utilisées par des compilateurs certifiés. On se préoccupe des aspects non déterministes, non définis ou d'autres peu spécifiés comme la gestion de la pile.
Stage à Paris
Stage au Laboratoire d'Informatique de Paris-Nord, sous la direction de Damiano Mazza et de Michele Pagani. Les types intersection qui caractérisent une grande classe de lambda-termes (l'ensemble des termes normalisables de tête) peuvent être vus comme un système de type issu de la logique linéaire multiplicative bien que cette dernière soit très restreinte.
rapport - slides CONCERTO - slides COMPLICE
Stage à Marseille
Stage au laboratoire d'informatique fondamentale, sous la direction de Rémi Eyraud. Les Contextual Binary Feature Grammars décrivent un langage formel à la manière d'une grammaire de Chomsky mais prenant en compte le contexte d'un mot pour spécifier la règle de dérivation associée. Cette représentation permet on l'espère d'extraire une structure sémantique sous-jacente (les non-terminaux d'une grammaire) d'un langage formel à partir d'une structure observable (les contextes).
Projet COQUILLE
COQUILLE est le "Projet Intégré" des M1IF de 2009/2010, ayant pour but de faciliter l'utilisation de coq notamment pour les résultats mathématiques. Le projet était constitué de différents groupes de travail, dont preuves (bibliothèques de preuves), apprentissage (de tactiques selon le contexte), et IDE (interface alternative à coqide en Qt).
Polys
Quelques polys de L3 rédigés par des élèves.Liens rapides
