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'Ehrhard¹⁾, 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 (présenté à TLLA 2017, Oxford, aux journées 2017 du Gdr Logique Linéaire, Rome et au séminaire Chocola de l'ENS Lyon), 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.

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_-_2017.pdf CV (en français) cv_-_2017_english_.pdf CV (in english).