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.

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

- 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.

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).