Papers by Lorenzo Tortora de Falco 

• Lorenzo Tortora de Falco Generalized standardization lemma for the additives (postcript) Electronic Notes in Theoretical Computer Science, Volume 3, Elsevier 1996.
  ABSTRACT: This is a preliminary report, in which we prove the so-called standardization lemma for the additives, in presence of a generalization (the natural one) of the commutative elementary reduction step. The technical tools developped to achieve this result suggest some remarks on the non confluence of full linear logic (without constants). 

• Myriam Quatrini, Lorenzo Tortora de Falco Polarisation des preuves classiques et renversement (postcript) Compte-Rendu de l'Académie des Sciences Paris, t.323, Série I, p.113-116, 1996.
  ABSTRACT: We introduce a new constraint on the proofs of the classical sequent \hspace{6em} calculus $LK^\eta_{pol}$ ($\eta$-constrained and polarized). We obtain a complete and \hspace{6em} stable fragment for which the $P$ embedding into linear logic is a decoration. 

• Jean-Baptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco Strong Normalization for `all-style' $LK^{tq}$ (postscript ) Lecture Notes in Artificial Intelligence 1071, p. 226-243, Springer-Verlag 1996.
  ABSTRACT: We prove strong normalization of $tq$-reduction for all standard versions of sequent calculus for classical and intuitionistic (first and second order) logic and give a perspicuous argument for the completeness of the focusing restriction on sequent derivations. 

• Lorenzo Tortora de Falco Denotational semantics for polarized (but non-constrained) $LK$ by means of the additives (postscript ) Lecture Notes in Computer Science, 1289 pp. 290-304 special issue for the proceedings of the conference ``$5^{th}$ Kurt Goedel Colloquium KGC'97, computational logic and proof theory", Wien (Austria) 25-29 august 1997, Springer-Verlag 1997.
  ABSTRACT: Following the idea that a classical proof is a superimposition of `constructive' proofs, we use the linear connective ``$\&$'' to define an embedding $P^a$ of polarized but non-constrained $LK$ in linear logic, which induces a denotational semantics. A classical cut-elimination step is now a cut-elimination step in one of the `constructive slices' superimposed by the classical proof. 

• Lorenzo Tortora de Falco Réseaux, cohérence et expériences obsessionnelles (postscript ) PhD thesis, Université Paris 7, january 2000.
  ABSTRACT: You can look at the table of contents 

• Lorenzo Tortora de Falco Coherent obsessional experiments for Linear Logic proof-nets (pdf ) The Bulletin of Symbolic Logic volume 7, Issue 1, p.154, march 2001.
  

• Lorenzo Tortora de Falco Additives of linear logic and normalization- Part I: a (restricted) Church-Rosser property ( postscript ) Theoretical Computer Science 294/3 pp. 489-524, february 2003.
  ABSTRACT: We define a generalized cut-elimination procedure for proof-nets of full linear logic (without constants), for which we prove a (restricted) Church-Rosser property. 

• Lorenzo Tortora de Falco Additives of linear logic and normalization- Part II: the additive standardization theorem (postscript ) preprint Quaderno I.A.C.-C.N.R. n. 10/2001, and submitted for publication.
  ABSTRACT: We prove the additive standardization theorem for full linear logic (without constants). 

• Jean-Baptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco SN and CR for free-style LK-tq: linear decorations and simulation of normalization ( postscript ), The Journal of Symbolic Logic 67 (1), march 2002, pp. 162-196
  ABSTRACT: The present report is a, somewhat lengthy, addendum to~\cite{DanJoiSche97}, where the elimination of cuts from derivations in sequent calculus for classical logic was studied `from the point of view of linear logic'. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between {\em multiplicative}\/ and {\em additive}\/ versions of the binary connectives. The main novelty here is the observation that this {\em type-distinction}\/ is not essential: we can allow classical sequent derivations to use {\em any}\/ combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of $tq$-reductions. We give a detailed description of the simulation of $tq$-reductions by means of reductions of the interpretation of any given classical proof as a proof net of {\bf PN2} (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of {\em one}\/ type, e.g.\ multiplicative. We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are {\em independent}: it is not possible to simulate them {\em internally}, i.e.\ by only {\em one}\/ specific combination, and structural rules. 

• Olivier Laurent, Myriam Quatrini, Lorenzo Tortora de Falco Polarized and focalized classical and linear proofs (preliminary version in postscript ), Annals of Pure and Applied Logic 134, Issues 2-3, pp. 217-263, july 2005
  ABSTRACT: We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs \cite{AndrPar,lc,lktq} are at the heart of our analysis: we show that the \tq-protocol of normalization (defined in \cite{lktq}) for the classical systems \LKe{} and \LKer{} perfectly fits normalization of polarized proof-nets. In section~\ref{isos}, some more semantical considerations allow to recover \LC{} as a refinement of multiplicative \LKe. 

• Lorenzo Tortora de Falco The additive multiboxes ( postscript ), Annals of Pure and Applied Logic 120, 1-3 pp. 65-102, january 2003
  ABSTRACT: We introduce the new notion of additive ``multibox'' for linear logic proof-nets. Thanks to this notion, we define a cut-elimination procedure which associates with every proof-net of multiplicative and additive linear logic a unique cut-free one. 

• Lorenzo Tortora de Falco Obsessional experiments for Linear Logic Proof-nets (preliminary version in postscript or in pdf ), Mathematical Structures in Computer Science 13, (Issue 6) pp. 799 - 855, december 2003
  ABSTRACT: We address the question of injectivity of coherent semantics of linear logic proof-nets. Starting from the definition of experiment given by Girard, we introduce the key-notion of ``injective obsessional experiment'', which allows to give a positive answer to our question for certain fragments of linear logic, and to build counter-examples to the injectivity of coherent semantics in the general case. 

• Olivier Laurent, Lorenzo Tortora de Falco Slicing polarized additive normalization ( postscript ) London Mathematical Society Lecture Note Series volume 316, pp. 247-282 Cambridge University Press 2004 (Book having as title "Linear Logic in Computer Science", Thomas Ehrhard, Jean-Yves Girard, Paul Ruet and Phil Scott editors)
  ABSTRACT: To attack the problem of ``computing with the additives'', we introduce a notion of sliced proof-net for the polarized fragment of linear logic. We prove that this notion yields computational objects, sequentializable in the absence of cuts. We then show how the injectivity property of denotational semantics guarantees the ``canonicity'' of sliced proof-nets, and prove injectivity for the fragment of polarized linear logic corresponding to simply typed lambda-calculus with pairing. 

• Lorenzo Tortora de Falco Sulla struttura logica del calcolo ( pdf ) Rendiconti di Matematica e delle sue Applicazioni. vol. VII (26), 2006
  ABSTRACT: Proponiamo una rassegna di alcuni aspetti degli sviluppi recenti della teoria della dimostrazione e dei suoi legami con l'informatica. 

• Olivier Laurent, Lorenzo Tortora de Falco Obsessional cliques: a semantic characterization of bounded time complexity ( postscript ) IEEE Computer Society Twenty-first annual IEEE symposium on Logic In Computer Science (LICS '06). August 2006.
  ABSTRACT: We give a semantic characterization of bounded complexity proofs. We introduce the notion of obsessional clique in the relational model of linear logic and show that restricting the morphisms of the category REL to obsessional cliques yields models of ELL and SLL. Conversely, we prove that these models are relatively complete: an LL proof whose interpretation is an obsessional clique is always an ELL/SLL proof. These results are achieved by introducing a system of ELL/SLL untyped proof-nets, which is both correct and complete with respect to elementary/polynomial time complexity. 

• Michele Pagani, Lorenzo Tortora de Falco Strong normalization property for second order linear logic ( pdf ) Theoretical Computer Science volume 411, issue 2, pp. 410-444, january 2010.
  ABSTRACT: The paper contains the first complete proof of strong normalization (SN) for full second order linear logic (LL): Girard's original proof uses a standardization theorem which is not proven. We introduce sliced pure structures (sps), a very general version of Girard's proof-nets, and we apply to sps Gandy's method to infer SN from weak normalization (WN). We prove a standardization theorem for sps: if WN without erasing steps holds for an sps, then it enjoys SN. A key step in the proof of standardization is a confluence theorem for sps obtained by using only a very weak form of correctness, namely acyclicity slice by slice. We conclude by showing how standardization for sps allows to prove SN of LL, using as usual Girard's reducibility candidates. 

• Daniel De Carvalho, Michele Pagani, Lorenzo Tortora de Falco A semantic measure of the execution time in Linear Logic ( pdf ) Theoretical Computer Science volume 412, issue 20, pp. 1884-1902, april 2011.
  ABSTRACT: We give a semantic account of the execution time (i.e. the number of cut-elimination steps leading to the normal form) of an untyped MELL (proof-)net. We first prove that: 1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then define a size on every experiment of a net, and we precisely relate the number of cut-elimination steps of every stratified reduction sequence to the size of a particular experiment. Finally, we give a semantic measure of execution time: we prove that we can compute the number of cut-elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the (untyped) lambda-calculus. 

• Daniel De Carvalho, Lorenzo Tortora de Falco The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings) ( pdf ) and a little Erratum ( pdf ) Annals of Pure and Applied Logic Volume 163, Issue 9, pp. 1210-1236, september 2012.
  ABSTRACT: We show that for a suitable fragment of linear logic the syntactical equivalence relation on proofs induced by cut-elimination coincide with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. More precisely, we prove that two cut-free proofs of the multiplicative and exponential fragment of linear logic with the same interpretation in the multiset based relational model are the same ``up to the connections between the doors of exponential boxes''. This result is proven in an untyped framework: two cut-free untyped Proof-Structures (PS) have the same Linear Proof-Structure (LPS). An immediate consequence is that two cut-free PS without weakenings with the same relational interpretation are the same; hence relational semantics is injective. 

• Pierre Boudes, Damiano Mazza, Lorenzo Tortora de Falco An Abstract Approach to Stratification in Linear Logic ( pdf ) Information and Computation Volume 241, pp. 32-61, april 2015.
  ABSTRACT: We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic. 

• Daniel de Carvalho, Lorenzo Tortora de Falco A semantic account of Strong Normalization in Linear Logic ( pdf ) Information and Computation Volume 248, pp.104-129, june 2016.
  ABSTRACT: We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly normalizable) compute the maximal length of the reduction sequences starting from that net. 

• Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco Computing connected proof(-structure)s from their Tayolr expansion ( pdf ) Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 20:1--20:18, ISBN 978-3-95977-010-1, 2016, proceedings of the conference ``Formal Structures for Computation and Deduction'', Porto (Portugal), 22-25 june 2016
  ABSTRACT: We show that every connected Multiplicative Exponential Linear Logic (MELL) proof-structure (with or without cuts) is uniquely determined by a well-chosen element of its Taylor expansion: the one obtained by taking two copies of the content of each box. As a consequence, the relational model is injective with respect to connected MELL proof-structures. 

• Lorenzo Tortora de Falco Editorial Preface ( pdf ) Mathematical Structures in Computer Science, Volume 28, 2018, special issue ``Differential Linear Logic, Nets, and other quantitative approaches to Proof-Theory''
  ABSTRACT: This special issue is devoted to some aspects of the new ideas that recently arose from the work of Thomas Ehrhard on the models of linear logic and of the lambda-calculus. 

• Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco Proof-net as graph, Taylor expansion as pullback ( pdf ) Lecture Notes in Computer Science, Volume 11541, pp. 282--300, ISBN 978-3-662-59532-9, 2019, proceedings of the conference ``26th Workshop on Logic, Language, Information and Computation (WoLLIC 2019)'', Utrecht (The Netherlands), 2-5 july 2019
  ABSTRACT: We introduce a new graphical representation for multiplicative and exponential linear logic proof-structures, based only on standard labelled oriented graphs and standard notions of graph theory. The inductive structure of boxes is handled by means of a box-tree. Our proof-structures are canonical and allows for an elegant definition of their Taylor expansion by means of pullbacks. 

• Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco Glueability of resource proof-structures: inverting the Taylor expansion ( pdf ) Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, ISBN 978-3-95977-132-0, 2020, proceedings of the conference ``28th edition of Computer Science Logic (CSL) '', the annual conference of the European Association for Computer Science Logic, Barcellona (Spain), 13-16 january 2020
  ABSTRACT: A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. 

• Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco Gluing resource proof-structures: inhabitation and inverting the Taylor expansion ( pdf ) Logical Methods in Computer Science, Volume 18, Issue 2, April 2022
  ABSTRACT: A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. As a consequence, we prove also semi-decidability of the type inhabitation problem for cut-free MELL proof-structures. 

• Adrien Ragot, Lorenzo Tortora de Falco, Thomas Seiller Linear Realisability over nets and second order quantification ( pdf ) Ceur Workshop Proceedings , Volume 3587, pp. 59--64, 2023, Proceedings of the 24th Italian Conference on Theoretical Computer Science, Palermo (Italy), September 13-15 2023
  ABSTRACT: We present a new realisability model based on othogonality for Linear Logic in the context of nets (untyped proof structures with generalized axiom). We show that it adequately models second order multiplicative linear logic. As usual, not all realizers are representations of a proof, but we identify specific types (sets of nets closed under bi-othogonality) that capture exactly the proofs of a given sequent. Furthermore these types are orthogonal of finite sets; this ensures the existence of a correctnesss criterion that runs in finite time. In particular, in the well known case of multiplicative linear logic, the types capturing the proofs are generated by the tests of Danos-Regnier, we provide - to our knowledge - the first proof of the folklore result which states ''test of a formula are proofs of its negation''.  

• Giulio Guerrieri, Giulia Manara, Lorenzo Tortora de Falco, Lionel Vaux Auclair Confluence for Proof Nets via Parallel Cut Elimination ( pdf ) Epic Series in Computing , Volume 100, pp. 464--483, proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Mauritius, May 26-31, 2024
  ABSTRACT: We provide the first proof of confluence for cut elimination in multiplicative-exponential linear logic proof-nets that is not based on Newman's lemma or strong normalization, not even indirectly. To achieve our goal, we take inspiration from Tait and Martin-Lof's method based on parallel reduction for the lambda-calculus, even though the wilder realm of untyped proof-nets makes the proof subtler and more challenging.