Rémi DI GUARDIA

I am a post-doc at IRIF (Paris) in the Preuves, programmes et systèmes (PPS) team. Currently, I work with Hugo Herbelin in the Malinca project around reasoning up to equivalent representations in Rocq.
Previously, in 2025, I researched on Quantum Bayesian Networks (a graphical syntax for probability theory exteneded to the quantum case) and their links with proof-nets (a graphical syntax for proofs in linear logic) with Claudia Faggian and Thomas Ehrhard, in the scope of the PEPR project EPiQ, at IRIF too.
Until the end of 2024, I was a PhD student in theoretical computer science at Ecole Normale Supérieure de Lyon in the Laboratoire de l'Informatique du Parallélisme (LIP), in the Plume team. My PhD was supervised by Olivier Laurent and focused on Linear Logic and in particular its proof-net syntax. It was financed by the LABEX MILYON.

My research subjets are proof theory, with a particular focus on proof-nets from linear logic, formalisation of proofs, graphical syntaxes (eg. string diagrams), and graph theory. I am broadly interested in the question of the identity of proofs.
As my current post-doc ends soon, I am looking for a new post-doc!

CV: English, Français
E-mail: remi \dot di \dot guardia \at ens-lyon \dot org OR diguardia \at irif \dot fr
Office: 4027

Publications

• Type Isomorphisms for Multiplicative-Additive Linear Logic
  With Olivier Laurent at LMCS
  After invitation, extended version of the FSCD 2023 article with the same name
  [ PDF | LMCS | HAL | ARXIV | DOI | BibTeX ]
  Abstract

  We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

  
  
• A Formalization of Multiplicative Proof-Nets in Rocq
  With Olivier Laurent at TLLA 2025
  [ PDF | Slides | HAL | Preprint | BibTeX | cf. Software Development ]
  Abstract

  We present an implementation of proof-nets for unit-free multiplicative linear logic in the proof assistant Rocq. It contains a definition of proof-structures and proof-nets, a proof of the sequentialization theorem as well as a definition of cut-elimination.

  
  
• Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
  With Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair at FSCD 2025
  [ PDF | Slides | HAL | HTML | DOI | BibTeX ]
  Abstract

  We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting par-vertex, on a splitting tensor-vertex, on a splitting terminal vertex, etc.
  The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.

  
  
• Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic
  Supervised by Olivier Laurent at Ecole Normale Supérieure de Lyon
  Defended on Sepember 23, 2024 in Salle des Thèses and online on BBB
  (The Manuscript has less typographical mistakes than what is available on HAL or Theses.fr.)
  [ Manuscript | Defense | HAL | Theses.fr | BibTeX ]
  
• Sequentialization is as fun as bungee jumping
  With Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair at TLLA 2023
  [ PDF | Slides | HAL | Preprint | BibTeX ]
  Abstract

  We propose a new proof of sequentialization for the proof nets of unit-free multiplicative linear logic with mix. It is based on the search of a splitting par by means of a simple new lemma about proof structures: the bungee jumping lemma.

  
  
• Type Isomorphisms for Multiplicative-Additive Linear Logic
  With Olivier Laurent at FSCD 2023 (see HAL for the full version with proofs)
  Superseded by its journal version
  [ PDF | Slides | HAL | DOI | BibTeX ]
  Abstract

  We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is given by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We then use the sequent calculus to extend our results to full MALL (including all units).

  
  
• Bottom-Up Sequentialization of Unit-Free MALL Proof Nets
  With Olivier Laurent at Linearity - TLLA 2022
  [ PDF | Slides (also on Easychair) | HAL | Preprint | BibTeX ]
  Abstract

  We propose a new proof of sequentialization for the proof nets of unit-free multiplicative-additive linear logic of Hughes & Van Glabbeek. This is done by adapting a method from unit-free multiplicative linear logic, showing the robustness of this approach.

  
  

Submissions

• Quantum Bayesian Networks: Compositionality and Typing via Linear Logic
  With Thomas Ehrhard and Claudia Faggian at FSCD 2026
  [ HAL ]
• Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
  With Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair at LMCS
  After invitation, extended version of the FSCD 2025 article with the same name
  [ ARXIV ]
  Abstract

  We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting vertex, which we can impose to be a par-vertex, or a terminal vertex, or a non-axiom vertex, etc., in a modular way. This approach applies in presence of the mix-rules as well as for proof nets of unit-free multiplicative-additive linear logic (through an appropriate further generalization of Yeo's theorem).
  The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.

Software Development

• Formalisation of the Proof-Nets of Multiplicative Linear Logic in Rocq (previously known as Coq), available on github (up-to-date), Software Heritage and HAL
  The sequentialization theorem is proved here (with no admit), but there still are some simplifications to be done. There also is a definition of cut-elimination, and a proof it terminates.

Unpublished Short Notes (not even in my thesis)

• Proof Equivalence in Linear Logic is Undecidable
  [ PDF ]
  Abstract

  Proofs of linear logic are often considered up to rule commutations. We prove that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable.

• Cut-Cut Commutations Are Not Superfluous
  [ PDF ]
  Abstract

  In the definition of a cut-elimination procedure, there often is a cut-cut commutation allowing to swap two cut-rules. This allows for instance to fully eliminate a chosen cut-rule without reducing other such rules in a proof. One may wonder whether such cut-cut steps are superfluous. We prove it is not the case in linear logic: some cut-free forms of a proof can only be reached using a cut-cut commutation. (Improved thanks to comments by Olivier Laurent.)

Talks

• Semantics and types for quantum Bayesian networks, Journées Informatique Quantique 2026, Bordeaux, 15 January 2026.
  [ Slides ]
  Abstract

  A general task of quantum theory is to predict the probabilities of measurement outcomes for a given system. In this sense, it can be framed as a problem of probabilistic inference over models involving both classical and quantum data. In the classical setting, Pearl’s Bayesian networks are a prominent graphical model to describe probability distributions in a compact way. They capture classical causality and enable efficient inference algorithms. The generalization of Bayesian networks to include quantum causes is an active line of research. We revisit some works in this line, specifically [Wood and Spekkens 2012, Leifer and Spekkens 2013, Henson Lal Pusey 2014], by bringing methods and concepts from proof-theory and the semantics of programming languages, which allows for typing and compositional reasoning. We propose a model which neatly encompasses both classical and quantum causal scenarios, while enabling the graphical methods typical of Bayesian networks. This allows in particular to study conditional independence (no-signaling) between random variables in a probability distribution, regardless of the fact that some of the causes are quantum. Our semantics adapts the one of [Selinger 2004] in order to obtain the following feature: when all causes are classical, the mathematical structure is the standard factors-based semantics of Bayesian networks, whereas in the fully quantum case it yields standard tensor-networks. Our graphical syntax, that is based on Linear Logic, is typed which allows for the composition of systems to be well-behaved.

• Confluence of Cut-elimination up to Rules commutations in Linear Logic, Seminar Syntax Meets Semantics, Paris, 8 January 2026.
  [ Slides ]
  Abstract

  This talk considers the identity of proofs: when are two proofs equal? Generally, syntactic equality is too constrained, and one wants to identify proofs (at least) up to cut-elimination - which is similar to identifying λ-terms up to β-reduction. This is the case, for instance, when considering a denotational model or when studying isomorphisms. We begin by giving intuitions for this problem in simply typed λ-calculus, where it is easily solved thanks to strong normalization and confluence of β-reduction. Then, we see which problems arise when trying to mimic this reasoning in Linear Logic. The main difficulty is that cut-elimination is only confluent up to an equivalence relation known as rule commutations, a result that is not easy to prove. In particular, it involves strong normalization of cut-elimination (and more), which is a known but far from trivial result in linear logic. We conclude by showing that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable. This entails that one cannot decide whether two proofs of linear logic are equal up to cut-elimination.

• Bayesian Networks and Proof-Nets: the proof-theory of Bayesian Inference, ArpiLYSM 2, Arpino, 11 November 2025.
  [ Slides ]
  Abstract

  Bayesian Networks are a graphical syntax describing probability distributions compactly by following dependencies of variables. I will present the correspondence between these Bayesian Networks and Proof Nets, a graphical syntax for proofs in linear logic. Uses of such a correspondence are giving a proof-theoretical account of Bayesian inference (in the spirit of the Curry-Howard correspondence), and exploiting the expressivity of Proof Nets to get compositional graphical methods where each intermediate graph is associated to a probability distribution. (Join work with Thomas Ehrhard and Claudia Faggian.)

• Confluence of Cut-elimination and Rules commutations in Linear Logic, Journées 2025 du GT Scalp, Vitry-sur-Seine, 29 October 2025.
  [ Slides ]
  Abstract

  This talk studies the identity of proofs: when are two proofs equal? Generally, syntactic equality is too constraint, and one wants to (at least) identify proofs up to cut-elimination - which is similar to identifying λ-terms up to β-reduction. We begin by giving intuitions for this problem in simply typed λ-calculus, where it is easily solved thanks to strong normalization and confluence of β-reduction. Then, we see which problems arise when trying to mimic this reasoning in Linear Logic. The main difficulty is that cut-elimination is only confluent up to an equivalence relation known as rule commutations, which is not easy to prove. We conclude by showing that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable.

• Cut-Expansion in Proof-Nets of Multiplicative Linear Logic, joint seminar of the LCS and LDP groups, Lumini, 9 October 2025.
  [ Slides ]
  Abstract

  Cut-elimination is a rewriting system defined in many logics, which has been widely studied. In general, a major result is to prove its weak normalization, which implies a provable formula always admits a cut-free proof. From this, various results can be more easily deduced: for instance that there is no proof of false. However, the reverse procedure - that we call cut-expansion - has been much less studied even though it is also useful! A goal here is the following: given a proof π with many cuts, can we find a proof π' with exactly one cut at its root and that reduces to π? Such a result has two applications. First, it allows to find a Craig's interpolant in the spirit of [Sau25,FOS25]. It is also useful in the case of a denotational semantic: while it is often clear how to interpret a single cut-rule between two proofs, it may not be the case for two proofs linked by "a bunch" of cut-rules - this problem was encountered e.g. in [EFP24]. We will present a very simple proof on how to apply cut-expansion steps to obtain only one cut-rule from a proof with many cut-rules in Multiplicative Linear Logic. We do so in the proof-net syntax as the proof is really easy to intuit in this formalism. We then use this result to immediately get a proof of Craig's interpolation. Lastly, and if time allows, we sketch how to extend our proof to full linear logic.
  [Sau25] Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. FSCD 2025. https://doi.org/10.4230/LIPIcs.FSCD.2025.32
  [FOS25] Guido Fiorillo, Daniel Osorio Valencia, and Alexis Saurin. On Correctness, Sequentialization and Interpolation. TLLA 2025.
  [EFP24] Thomas Ehrhard, Claudia Faggian, and Michele Pagani. Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference. Technical Report. https://doi.org/10.48550/arXiv.2412.20540

• A Formalization of Multiplicative Proof-Nets in Rocq, TLLA 2025, Birmingham, 19 July 2025.
  [ Slides | cf. Publications ]
  Abstract

  We present an implementation of proof-nets for unit-free multiplicative linear logic in the proof assistant Rocq. It contains a definition of proof-structures and proof-nets, a proof of the sequentialization theorem as well as a definition of cut-elimination.

• Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic, FSCD 2025, Birmingham, 18 July 2025.
  [ Slides | cf. Publications ]
  Abstract

  We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting par-vertex, on a splitting tensor-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.

• Identity of Proofs and Formulas in Linear Logic, Journées PPS 2025, Paris, 1 July 2025.
  [ Slides ]
  Abstract

  In a logical system, deciding whether two proofs, or two formulas, are equal is often complicated. Indeed, one usually does not want to identify only proofs that are syntactically equal, i.e. whose rules are exactly the same. In many sequent calculi, there is a cut rule that allows for computation - through a process called cut-elimination - and one wishes for two proofs related by such a computation to be equivalent. Looking at programs through the Curry-Howard correspondence, even if 2 + 2 and (1 + 2) + 1 are not strictly the same term, it is still very sensible to identify them. Another notion of identity on proofs is axiom-expansion, corresponding to the fact that a function f should be considered the same as x ↦ f(x), the function that takes an input x and returns f(x), which is again very natural to ask for. Hence, proofs are seen as equivalent up to these two relations (at least), which in many logical systems is either a trivial nonsense or a combinatorial nightmare. Furthermore, these equalities between proofs yield a notion of equality between formulas, called isomorphism. Two formulas A and B are isomorphic if there are proofs between them whose compositions yield identities - up to the above equivalence relations. Intuitively, this means there is a loseless encoding between A and B, and thus they can be considered as the same; for instance, every use of A can be replaced with one use of B. I will present and give a survey of these two problems of equalities in the framework of linear logic.

• Identity of formulas and proofs, PACM∧N 2025, Rome, 16 May 2025.
  [ Slides ]
  Abstract

  In a logical system, deciding whether two proofs (or two formulas) are equal is usually complicated. Indeed, one usually does not want to identify only proofs that are syntactically equal, i.e. whose rules are exactly the same. In many sequent calculi, there is a cut rule that allows for computation - through a process called cut-elimination - and one wishes for two proofs related by such a computation to be the same. Looking at programs through the Curry-Howard correspondence, even if 2 + 2 and (1 + 2) + 1 are not strictly the same term, it is still very sensible to identify them. Another notion of identity on proofs is axiom-expansion, corresponding to the fact that a function f should be considered the same as x ↦ f(x), the function that takes an input x and returns f(x), which is again very natural to ask for. Hence, proofs are seen as equivalent up to these two relations, which in general is either a trivial nonsense or a combinatorial nightmare. Furthermore, these equalities between proofs yield a notion of equality between formulas, called isomorphism. Two formulas A and B are isomorphic if there are proofs between them whose compositions yield identities - up to the above equivalence relations. Intuitively, this means there is a loseless encoding between A and B, and thus they can be considered as the same; for instance, every use of A can be replaced with one use of B. I will present this problem of equalities, in the setting of lambda-calculus and linear logic, along with some known results and difficulties.

• Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic, Kickoff meeting of the IRN-LI, Rome, 12 May 2025.
  [ Slides ]
  Abstract

  We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting par-vertex, on a splitting tensor-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges); similar results from the literature required more involved encodings.
  (Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair.)

• Une formalisation en Rocq/Coq des réseaux de preuve de la logique linéaire, Groupe de travail of the IGG team of ICube, Strasbourg, 3 April 2025.
  [ Slides ]
  Abstract (in French)

  Les réseaux de preuve sont une contribution majeure de la logique linéaire. Contrairement aux représentations usuelles des preuves comme des arbres de dérivation, un réseau représente une preuve comme un graphe respectant certaines contraintes. Cette syntaxe graphique a de meilleures propriétés, mais n'est pas inductive. Cela explique que malgré une littérature pléthorique sur papier, il y a très peu de formalisations dans des assistants de preuve sur ce sujet : l'obstacle principal est la manipulation de (multi-)graphes sur ordinateur. Je vais présenter une formalisation de ces objets en Rocq/Coq, avec leur définition et quelques résultats standards. En particulier, je vais appuyer sur les difficultés rencontrées et les solutions trouvées en réponse.
  (Travail issu majoritairement de ma thèse, supervisée par Olivier Laurent.)

• A simple proof of sequentialization for proof-nets, and links with graph theory, Groupe de travail of the Sémantique team of IRIF, Paris, 28 January 2025.
  [ On blackboard ]
  Abstract

  Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyen but focusing on edge-colored graphs instead of perfect matchings.
  (Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair.)

• Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic, PhD Defense, Lyon, 23 September 2024.
  [ Slides | cf. Publications ]
• Autour du théorème de Yeo, Groupe de travail of the Plume team of LIP, Lyon, 24 June 2024.
  [ On blackboard ]
  Abstract (in French)

  Cet exposé présentera une preuve simple du théorème de Yeo [1], après avoir donné les usuelles notions de théorie des graphes nécessaires (chemin, cycle, coloriage d'arêtes, ...). Cette démonstration est basée sur un nouveau résultat facile à montrer : le saut à l'élastique. Je discuterai ensuite rapidement, si le temps le permet, de généralisations et d'applications de ce théorème.
  [1] Anders Yeo. "A Note on Alternating Cycles in Edge-Coloured Graphs". In: Journal of Combinatorial Theory, Series B 69.2 (1997), pp. 222-225.

• Retractions in Multiplicative Linear Logic, Chocola, Lyon, 14 March 2024.
  [ Slides ]
  Abstract

  Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be. I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.

• Retractions in Multiplicative Linear Logic, Group Seminar of the Mathematical Foundations of Computation team of the University of Bath, Bath, 1 March 2024.
  [ Slides ]
  Abstract

  Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be. I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.

• Retractions for Multiplicative Linear Logic, Journées 2023 du GT Scalp, Orléans, 29 November 2023.
  [ Slides ]
  Abstract (in French)

  Je vais parler de rétraction en logique. Pour des formules A et B, A est une rétraction de B s'il existe des preuves de A |- B et B |- A dont la composition par coupure sur B est égale à l'axiome sur A, à élimination des coupures et expansion des axiomes près. Cela correspond aux rétractions dans la catégorie des preuves : les objets sont des formules, les morphismes des preuves (considérées à élimination des coupures et expansion des axiomes près), la composition est la coupure et les identités les axiomes. Alors que les isomorphismes de MLL sont connus (Balat et Di Cosmo ont donné une théorie équationnelle correspondante), et qu'il y a une rétraction (qui n'est pas un isomorphisme) de bien connue, il n'y a même pas d'hypothèse sur ce que pourraient être l'ensemble des rétractions. Je vais présenter un travail en cours sur les rétractions de la forme "un atome X est une rétraction de B", et quelles sont les difficultés pour étendre ce résultat au cas de formules quelconques.

• Type Isomorphisms for Multiplicative-Additive Linear Logic, FSCD 2023, Rome, 4 July 2023.
  [ Slides | cf. Publications ]
  Abstract

  We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is given by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We then use the sequent calculus to extend our results to full MALL (including all units).

• Sequentialization is as fun as bungee jumping, TLLA 2023, Rome, 1 July 2023.
  [ Slides | cf. Publications ]
  Abstract

  We propose a new proof of sequentialization for the proof nets of unit-free multiplicative linear logic with mix. It is based on the search of a splitting par by means of a simple new lemma about proof structures: the bungee jumping lemma.

• Proof theory and linear logic, PhD student's seminar of LIP, Lyon, 27 June 2023.
  [ Slides ]
• A simple proof of sequentialization for MLL proof nets, Groupe de travail of the Plume team of LIP, Lyon, 15 May 2023.
  [ On blackboard ]
  Abstract

  We will present proof nets for unit-free multiplicative linear logic (MLL) before giving a new simple proof of the sequentialization theorem, the key result affirming that proof-nets do indeed represent proofs. This simple proof holds in the presence of the mix rule, and is robust enough to be adapted to proof nets with the additive connectives.

• Type isomorphisms for Multiplicative-Additive Linear Logic, Groupe de travail of the Plume team of LIP, Lyon, 10 October 2022 & 7 November 2022.
  [ On blackboard ]
  Abstract

  We will speak about isomorphisms in logic. Two formulas A and B are isomorphic if there are proofs of A |- B and of B |- A such that their composition by cut over B (resp. A) is equal to the axiom of A (resp. B) up to cut elimination and axiom expansion. This corresponds to isomorphisms in the category of proofs: objects are formulas, morphisms are proofs (up to cut elimination and axiom expansion), composition is cut and identities are axioms. The problem of characterizing isomorphisms in Multiplicative Linear Logic was already solved by Balat and Di Cosmo. They proved that isomorphisms correspond to associativity and commutativity of the connectives tensor and par, as well as neutrality of the units one and bottom. Their proof uses in an essential way proof nets, an alternative representation of proofs with respect to proof trees. The case of Multiplicative-Additive Linear Logic, with the additive connectives plus and with, is more complex because of the distributive laws of the tensor over the plus and of the par over the with. During this presentation, we will introduce the notion of isomorphism in different settings, before giving an overview of the proof from Balat and Di Cosmo and then explaining how to extend it in the presence of additives.

• Bottom-Up Sequentialization of Unit-Free MALL Proof Nets, Linearity - TLLA 2022, Haifa, 31 July 2022.
  [ Slides | cf. Publications ]
  Abstract

  We propose a new proof of sequentialization for the proof nets of unit-free multiplicative-additive linear logic of Hughes & Van Glabbeek. This is done by adapting a method from unit-free multiplicative linear logic, showing the robustness of this approach.

Teaching

• 2023 - 2024
  • Architecture des ordinateurs, lectured by Sylvain Brandel (L2 at Université Claude Bernard Lyon 1)
  • Logique, lectured by Natacha Portier (L3 at Ecole Normale Supérieure de Lyon)
• 2022 - 2023
  • Compilation and Program Analysis, lectured by Gabriel Radanne and Ludovic Henrio (M1 at Ecole Normale Supérieure de Lyon)
  • Functional Project, lectured by Daniel Hirschkoff (L3 at Ecole Normale Supérieure de Lyon)
• 2021 - 2022
  • Compilation and Program Analysis, lectured by Gabriel Radanne and Ludovic Henrio (M1 at Ecole Normale Supérieure de Lyon)
  • Functional Project, lectured by Daniel Hirschkoff (L3 at Ecole Normale Supérieure de Lyon)
• I also gave a proof of sequentialization for proof-nets of multiplicative linear logic during the lectures of Claudia Faggian for LMFI 2024/2025 and MPRI 2025/2026.
  [ Slides ]