I am 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 is supervised by Olivier Laurent and is focused on Linear Logic and in particular its proof-net syntax.
CV: English, Français
E-mail: remi \dot di-guardia \at ens-lyon \dot fr
Office: M7 311
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.
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 parr, 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 parr 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.