PhD thesis

• Project with Thomas Seiller: succeeding the Geometry of Interaction, the “Transcendental Syntax” project of Jean-Yves Girard aims at a reconstruction of logical entities (LL proof-nets, formulas, correctness criterion, truth/provability) from a model of computation based on first-order unification. The project suggests a new and fully computational foundation for linear logic.

• Project with Damiano Mazza: we study how the Geometry of Interaction can be used a relevant tool for the analysis of space complexity for the lambda-calculus. Moreover, we study how linear terms can “approximate” the lambda-calculus and how it is related to the approximation of Turing machines by boolean circuits. We would like to relate the computational complexity of lambda terms to the ones of Turing machines in order to provide characterisations of complexity classes within lambda-calculus.

Publications

• Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation (April 2016) with Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce. CSF 2016.
• A gentle introduction to Girard’s Transcendental Syntax (June 2021) with Thomas Seiller. TLLA 2021 (workshop).

Unpublished works

• Multiplicative linear logic from a resolution-based tile system with Thomas Seiller [Unpublished] (July 2022).
• A gentle introduction to Girard’s Transcendental Syntax for the linear logician [Unpublished] (May 2021).

Presentations (slides PDF)

• Introduction à la Géométrie de l’Interaction. ReFL seminar, February 2023 (online), 35min.
• Transcendental Syntax: a toolbox for the interface logic-computation. GT Scalp. November 2021 Fontainbleau, 20min.
• A technical reading of the Transcendental Syntax. LDP Seminar. September 2021 Marseille, 90min.
• Entretien de suivi de thèse. September 2021 Villetaneuse, 30min.
• A gentle introduction to Girard’s Transcendental Syntax. TLLA 2021, June 2021 Roma (online), 15min. [Extended abstract]
• From computation to a reconstruction of (linear) logic. Midlands Graduate School 2021, April 2021 Midlands (online), 10-15min.
• Transcendental Syntax - The dynamics of logic programs and tilings, applied to Linear Logic. LIPN Seminar, March 2021 Villetaneuse (online), 70-80min.
• A taste of Girard’s Transcendental Syntax. Workshop Proof-Nets, January 2021 Montpellier (online), 20min.

Working group

• ReFL (Réflexions sur les Fondements de la Logique)

PhD thesis

An exegesis of transcendental syntax. Available on HAL.

Internship reports

All documents are written in French.

• De la Géométrie de l’Interaction à la Syntaxe Transcendentale (2019/incomplete) with Thomas Seiller.
  [report] [slides] [subject]
• Sur l’espace des termes et des machines (2018/incomplete) with Damiano Mazza.
  [report] [slides]
• Etude du langage PCF à travers les réseaux de preuve de la logique linéaire (2017) with Michele Pagani and Delia Kesner.
  [report]
• Formalisation des garanties de sécurité apportées par l’isolation de composants logiciels (2016) with Yannis Juglaret.
  [report] [slides] [source]