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 ), 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 ) Rapport Institut National de Recherche en Informatique et Automatique n.6441, january 2008, and to appear in Theoretical Computer Science.
  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 ) Preprint, February 2010.
  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.