Ceci est une ancienne révision du document !


Recherche

Je suis actuellement doctorant dans l'équipe PPS de l'irif (2016-2019) où je travaille avec Alexis Saurin et Christine Tasson, mais la première partie de la thèse s'est déroulée dans l'équipe LdP de l'I2M à Marseille, où je travaillais plus particulièrement avec Lionel Vaux.

Mes centres d'intérêt se concentrent autour de la théorie de la démonstration, et en particulier sur la logique linéaire et le λ-calcul dont j'étudie les approches différentielles introduites par Ehrhard et Régnier. Mon étude se concentre précisément sur le développement de Taylor que ces extensions permettent d'exprimer.

A la suite du stage que j'avais déjà effectué avec Lionel Vaux à Luminy (pour le master LMFI de Paris-Diderot), je m'efforce d'utiliser une syntaxe particulière pour étudier les réseaux de preuve issue d'un article d'Ehrhard1), et qui permet l'étude du développement de Taylor des réseaux dans un cadre formel.

Suite à un résultat encourageant sur les réseaux dans ce sens (qui a été l'objet d'une publication à CSL2018), j'étudie différents systèmes (lambda calculs étendus, PCF, Call-by-Push-Value,…) pour y développer et examiner les calculs à ressources associés dans d'autres contextes.

An application of parallel cut elimination in unit-free multiplicative linear logic to the Taylor expansion of proof nets https://hal.archives-ouvertes.fr/hal-01835242/document (Avec Lionel Vaux Auclair, à paraître dans les actes de CSL 2018.)

Et les transparents de son exposé (3 septembre 2018, Birmingham) : csl2018.pdf

Enseignement

Dans le cadre de mon doctorat, j'ai été chargé (au deuxième semestre 2017-2018) des enseignements suivants :

- Outils pour l'analyse d'algorithmes (EA4, TD et TP), cours de L2 d'informatique approchant la complexité algorithmique avec des notions mathématiques, et des applications : implémentations en python.

- Concepts informatiques (CI2, TD), cours de L1 d'informatique donnant une approche de la compilation, de la traduction de programmes, et de la description de l'état de la mémoire lors de l'exécution de programmes écrits en java.

Et au premier semestre 2018-2019 :

- Initiation à la programmation (TP), java, cours de L1

-Bases de données (TP), cours de L2

Documents

chocola_2017.pdf Transparents de mon exposé sur la normalisation du développement de Taylor des réseaux, séminaire CHoCoLa, ENS Lyon, 9/11/2017.
tlla17.pdf
transparents de mon exposé sur la normalisation par évaluation dans les réseaux de preuve, Oxford, 3/09/2017, TLLA2017.

memoire_m2.pdf Exponentielles et connexité dans les réseaux à la Ehrhard. Mémoire de stage de M2 (LMFI) dirigé par Lionel Vaux et effectué à l'I2M au printemps 2015.

memoire_jc_identite_des_preuves.pdf L'identité des preuves : normalisation, réseaux et séparation. Mémoire de M2 (LOPHISC) réalisé en 2016 à Paris 1-Panthéon-Sorbonne dirigé par Jean Fichot. Lien hal : https://hal-paris1.archives-ouvertes.fr/dumas-01427107v1

cv_2018.pdf CV (en français) cv_2018_english_.pdf CV (in english).


1)
2014, A new correctness criterion for MLL proof nets