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) through a model of computation based on first-order unification. The project suggests a new and fully computational foundation for 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 classes within a lambda-calculus.

Current research directions: computation with interactive hypergraphs, geometric tilings, approximation of computation, geometry of interaction and automata theory, geometry of interaction and implicit computational complexity, links between logic and functional programming, representations of proofs.

Secondary research interests: quantum computation, homotopy type theory, realizability, linguistics, bioinformatics, ludics, game semantics, history of logic.

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.

Unpublished works

• Multiplicative Linear Logic from Logic Programs and Tilings (January 2021) with Thomas Seiller.
• Stellar Resolution: Multiplicatives - for the linear logician through examples (October 2020).

Presentations (slides PDF)

• (Title soon). Séminaire LIPN, Mars 2021 Université Sorbonne Paris Nord (online).
• A taste of Girard’s Transcendental Syntax. Workshop Proof-Nets, Janvier 2021 Montpellier (online), 20min.

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]