Je suis maître de conférences en mathématiques
(HDR)
à l'université d’Aix-Marseille
depuis septembre 2009. J'ai rejoint l'équipe LDP
de l'I2M
(ex-IML)
après une
thèse de mathématiques dans cette équipe,
suivie d'une année d'ATER en informatique à l'université de Savoie.
De septembre 2011 à août 2014, j’ai été directeur de l'IREM d'Aix-Marseille. Je continue à m’y occuper, entre autres, de l’enseignement de l’informatique dans le secondaire, notamment avec l’organisation d’une journée académique annuelle. Et j’y anime régulièrement des stages Hippocampe en mathématiques.
J’organise le séminaire Logique et Interactions de l’I2M depuis septembre 2014.
Je suis responsable de l’équipe LDP depuis janvier 2018.
Mes intérêts de recherche se situent à l'interface entre informatique et logique. Mon domaine de prédilection est la théorie de la démonstration, éclairée par la correspondance preuves-programmes.
Plus précisément, mes activités de recherche à ce jour sont concentrées autour de trois domaines distincts mais intimement connectés:
Mes articles sont disponibles sur ce site. Une description de ma thèse et les documents associés se retrouvent sur une page dédiée. On peut également consulter la liste donnée par DBLP.
Je participe régulièrement aux séminaires Chocola, des rencontres mensuelles organisées à l’ÉNS de Lyon sur la correspondance de Curry-Howard et les thèmes connexes.
Depuis l'été 2010, Emmanuel Beffara et moi mettons en place une gestion durable du tableau noir (et comme pour presque toute démarche de développement durable, c’est déjà un échec).
Je suis membre du réseau de recherche international de Logique Linéaire.
Je suis co-responsable avec Samuel Mimram du groupe de travail LHC du GDR Informatique Mathématique. Je suis également membre du groupe de travail Scalp du même GDR.
J’étais coordinateur du projet PEPS QuAND, financé par l’INS2I en 2010 et 2011, et membre des projets Choco, Récré, Logoi, Loci et CoQuaS financés par l'ANR les années passées.
Entre autres:
