Search

Your search keyword '"Tortora de Falco, Lorenzo"' showing total 11 results
Start Over Author "Tortora de Falco, Lorenzo" Publisher hal ccsd
11 results on '"Tortora de Falco, Lorenzo"'

1. MELL proof-nets in the category of graphs

Author

Guerrieri, Giulio, Manara, Giulia, Pellissier, Luc, Tortora de Falco, Lorenzo, Vaux Auclair, Lionel, Gouat, Isabelle, Lionel Vaux Auclair, Victoria Barrett, Etienne Callies, Kostia Chardonnet, Bruno Dinis, Thomas Ehrhard, Boris Eng, Claudia Faggian, Lorenzo Tortora de Falco, Giulio Guerrieri, Alessio Guglielmi, Jack Hughes, Farzad Jafarrahmani, Olivier Laurent, Roberto Maieli, Giulia Manara, Daniel Marshall, Paulin Jacobé de Naurois, Paulo Oliva, Dominic Orchard, Luc Pellissier, Alexis Saurin, Thomas Seiller, Siva Somayyajula, Riccardo Treglia, Benoît Valiron, Renaud Vilmart, James Wood, Guerrieri, Giulio, Manara, Giulia, Pellissier, Luc, TORTORA DE FALCO, Lorenzo, Vaux Auclair, Lionel, University of Bath [Bath], Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Università degli Studi Roma Tre, and Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Proof-nets, Linear Logic, Category theory, Graph theory
Abstract

International audience; We present a formalization of proof-nets (and more generally, proofstructures) for the multiplicative-exponential fragment of linear logic, with a novel treatment of boxes: instead of integrating boxes into to the graphical structure (e.g., by adding explicit auxiliary doors, plus a mapping from boxed nodes to the main door, and ad hoc conditions on the nesting of boxes), we fix a graph morphism from the underlying graph of the proof-structure to the tree of boxes given by the nesting order. This approach allows to apply tools and notions from the theory of algebraic graph transformations, and obtain very synthetic presentations of sophisticated operations: for instance, each element of the Taylor expansion of a proof-structure is obtained by a pullback along a morphism representing a thick subtree of the tree of boxes. A treatment of cut elimination in this framework currently under development.

Published
2021

2. Glueability of resource proof-structures: inverting the Taylor expansion

Author

Guerrieri, Giulio, Pellissier, Luc, Tortora De Falco, Lorenzo, University of Bath [Bath], Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Dipartimento di Matematica e Fisica [Roma], Università degli Studi Roma Tre, Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco, Guerrieri, G., Pellissier, L., Tortora De Falco, L., and Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)

Subjects
060201 languages & linguistics, 000 Computer science, knowledge, general works, Natural transformation, Taylor expansion, Proof-net, Linear logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 06 humanities and the arts, 02 engineering and technology, proof-structure, proof-net, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, linear logic, 0602 languages and literature, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing
Abstract

International audience; A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a (infinite) 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.

Published
2020

3. Finite semantics of polymorphism, complexity and the power of type fixpoints

Author

Nguyễn, Lê Thành Dũng, Seiller, Thomas, Pistone, Paolo, Tortora De Falco, Lorenzo, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), Wilhelm-Schickard-Institut für Informatik [Tübingen], Eberhard Karls Universität Tübingen = Eberhard Karls University of Tuebingen, Dipartimento di Matematica [Roma TRE], and Università degli Studi Roma Tre

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

Many applications of denotational semantics, such as higher-order model checking or the complexity of normaliza-tion, rely on finite semantics for monomorphic type systems. We present two constructions of finite semantics for second-order Multiplicative-Additive Linear Logic (MALL2) and study their properties. We apply this to understand the gap in expressive power between MALL2 and its extension with type fixpoints, and to obtain an implicit characterization of regular languages in Elementary Linear Logic. Furthermore, some semantic results established here lay the groundwork for a sequel paper proposing a new approach to sub-polynomial implicit complexity.

Published
2019

4. Computing connected proof(-structure)s from their Taylor expansion

Author

Giulio Guerrieri, Luc Pellissier, TORTORA DE FALCO, LORENZO, Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Gruppo di Logica, Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre-Università degli Studi Roma Tre, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Delia Kesner, Brigitte Pientka, ANR-14-CE25-0005,ELICA,Élargir les idées logiques pour l'analyse de complexité(2014), ANR-12-JS02-0006,CoQuaS,Calculer avec la Sémantique Quantitative(2012), ANR-11-IS02-0002,Locali,Approche Logique de Nouveaux Paradigmes de Calcul(2011), ANR-11-IDEX-0001,Amidex,INITIATIVE D'EXCELLENCE AIX MARSEILLE UNIVERSITE(2011), Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)-Università degli Studi Roma Tre = Roma Tre University (ROMA TRE), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco, Giulio, Guerrieri, Luc, Pellissier, and TORTORA DE FALCO, Lorenzo

Subjects
000 Computer science, knowledge, general works, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory, Taylor expansion, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, Proof-structures, 01 natural sciences, Linear Logic, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems, Proof-nets, 010201 computation theory & mathematics, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Relational semantics
Abstract

International audience; 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.

Published
2016

5. Relational type-checking for MELL proof-structures. Part 1: Multiplicatives

Author

Guerrieri, Giulio, Pellissier, Luc, Tortora De Falco, Lorenzo, Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Gruppo di Logica, Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)-Università degli Studi Roma Tre = Roma Tre University (ROMA TRE), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), ANR-12-JS02-0006,CoQuaS,Calculer avec la Sémantique Quantitative(2012), ANR-14-CE25-0005,ELICA,Élargir les idées logiques pour l'analyse de complexité(2014), Università degli Studi Roma Tre-Università degli Studi Roma Tre, and Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, relational semantics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], type-checking, Linear Logic, Logic in Computer Science (cs.LO), denotational semantics
Abstract

Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $\Gamma$ acts thus as a type (refining $\Gamma$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $\Gamma$, and a point x in the relational interpretation of $\Gamma$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it in time linear in the size of R, if R is a proof-structure in the multiplicative fragment of linear logic. This algorithm can be extended to larger fragments of multiplicative-exponential linear logic containing $\lambda$-calculus.

Published
2016

6. Relational type-checking of connected proof-structures

Author

Guerrieri, Giulio, Pellissier, Luc, Tortora de Falco, Lorenzo, Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Gruppo di Logica, Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre-Università degli Studi Roma Tre, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), ANR-12-JS02-0006,CoQuaS,Calculer avec la Sémantique Quantitative(2012), ANR-14-CE25-0005,ELICA,Élargir les idées logiques pour l'analyse de complexité(2014), Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)-Università degli Studi Roma Tre = Roma Tre University (ROMA TRE), and Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)

Subjects
relational interpretation, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], semantic typing, relational interaction abstract machine
Abstract

International audience; It is possible to define a typing system for Multiplicative Exponential Linear Logic (MELL): in such a system, typing judgments are of the form ⊢ R : x : Γ, where R is a MELL proof-structure, Γ is the list of types of the conclusions of R, and x an element of the relational interpretation of Γ, meaning that x is an element of the relational interpretation of R (of type Γ).As relational semantics can be used to infer execution properties of the proof-structure, these judgment can be considered as forms of quantitative typing.We provide an abstract machine that decides, if R satisfies a geometric condition, whether the judgment ⊢ R : x : Γ is valid. Also, the machine halts in bilinear time in the sizes of R and x.

Published
2016

7. Injectivity of relational semantics with respect to MELL proof-nets and the Taylor expansion

Author

Guerrieri, Giulio, Pellissier, Luc, Tortora De Falco, Lorenzo, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS), Gruppo di Logica, Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre-Università degli Studi Roma Tre, and Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2015

8. Injectivity of relational semantics for (connected) MELL proof-nets via Taylor expansion

Author

Guerrieri, Giulio, Tortora De Falco, Lorenzo, Pellissier, Luc, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Gruppo di Logica, Dipartimento di Matematica e Fisica, Università degli Studi Roma Tre-Università degli Studi Roma Tre, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), and École normale supérieure - Cachan (ENS Cachan)

Subjects
proof-nets, relational semantics, Taylor expansion, differential linear logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], denotational semantics
Abstract

International audience; We show that: (1) the Taylor expansion of a cut-free MELL proof-structure R with atomic axioms is the (most informative part of the) relational semantics of R; (2) every (connected) MELL proof-net is uniquely determined by the element of order 2 of its Taylor expansion; (3) the relational semantics is injective for (connected) MELL proof-nets.

Published
2014

9. A semantic measure of the execution time in Linear Logic

Author

De Carvalho, Daniel, Pagani, Michele, Tortora De Falco, Lorenzo, Linear logic, proof networks and categorial grammars (CALLIGRAMME), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Filosofia dell'Universita Roma Tre, Università degli Studi Roma Tre, Partially supported by project NO-CoST (ANR, JC05\_43380), INRIA, Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)

Subjects
proof-nets, linear logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], implicit computational complexity, denotational semantics
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.

Published
2008

10. Obsessional cliques: a semantic characterization of bounded time complexity

Author

Olivier Laurent, L.T. de Falco, Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Filosofia, Università degli Studi Roma Tre, Supported by the project ``Coop. Italia/France CNR-CNRS n°19188'. Supported by the French project ``ANR JC05_43380 No-Cost'. Supported by the Italian project ``FOLLIA', Rajeev Alur, Laurent, O, and TORTORA DE FALCO, Lorenzo

Subjects
Clique, Discrete mathematics, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Implicit Computational Complexity, computational complexity, Computational complexity theory, Proof-net, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, Mathematical proof, 01 natural sciences, Linear logic, Combinatorics, Automated theorem proving, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], Morphism, 010201 computation theory & mathematics, Bounded function, linear logic, Obsessional cliques, 0101 mathematics, Time complexity, Mathematics, denotational semantics
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 RscrEscrLscr 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

Published
2006

11. Slicing polarized additive normalization

Author

Olivier Laurent, Lorenzo Tortora de Falco, Institut de mathématiques de Luminy (IML), Centre National de la Recherche Scientifique (CNRS)-Université de la Méditerranée - Aix-Marseille 2, Dipartimento di Filosofia, Università degli Studi Roma Tre, Thomas Ehrhard and Jean-Yves Girard and Paul Ruet and Philip Scott, Laurent, O, TORTORA DE FALCO, Lorenzo, Université de la Méditerranée - Aix-Marseille 2-Centre National de la Recherche Scientifique (CNRS), and Università degli Studi Roma Tre = Roma Tre University (ROMA TRE)

Subjects
Normalization (statistics), Computer science, 010102 general mathematics, Computational logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 16. Peace & justice, Symbolic computation, additive proof-net, 01 natural sciences, Slicing, Linear logic, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Algorithmics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, 0101 mathematics, Algorithm, polarities
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 the simply typed lambda-calculus with pairing.

Published
2004

Catalog

Books, media, physical & digital resources
See catalog results