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.
I am a post-doc at IRIF (Paris) in the Preuves, programmes et systèmes (PPS) team.
My supervisor is Claudia Faggian, and I also work with Alexis Saurin and Thomas Ehrhard.
I was hired thanks to the PEPR project EPiQ to study graphical syntaxes.
Until September 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.
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.
CV: English, Français
E-mail: diguardia \at irif \dot fr (warning: my @ens-lyon.fr e-mail does not work anymore, even if it does not send back any error message!)
Office: 3028
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.
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).
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.
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.
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.
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.)
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]
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.
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.
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.
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.
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.
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.