39 results on '"Tortora de Falco, Lorenzo"'
Search Results
2. An abstract approach to stratification in linear logic
- Author
-
Boudes, Pierre, Mazza, Damiano, and Tortora de Falco, Lorenzo
- Published
- 2015
- Full Text
- View/download PDF
3. The relational model is injective for multiplicative exponential linear logic (without weakenings)
- Author
-
de Carvalho, Daniel and Tortora de Falco, Lorenzo
- Published
- 2012
- Full Text
- View/download PDF
4. 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
5. Strong normalization property for second order linear logic
- Author
-
Pagani, Michele and Tortora de Falco, Lorenzo
- Published
- 2010
- Full Text
- View/download PDF
6. Preface Special Issue: Differential Linear Logic, Nets and Other Quantitative and Parallel Approaches to Proof-Theory
- Author
-
TORTORA DE FALCO, LORENZO, Ehrhard T., Tasson C., Vaux L., Mazza D., Beffara E., de Carvalho D., Di Giamberardino P., Melliès P.-A., Tabareau N., Tortora de Falco Lorenzo, and TORTORA DE FALCO, Lorenzo
- Subjects
Mathematics (miscellaneous) ,Computer Science Applications1707 Computer Vision and Pattern Recognition - 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 (LL) and of the λ-calculus. In some sense, the very origin of these ideas dates back to the introduction of LL in the 80s by Jean-Yves Girard. An obvious remark is that LL yielded a first logical quantitative account of the use of resources: the logical distinction between linear and non-linear formulas through the introduction of the exponential connectives. As explicitly mentioned by Girard in his first paper on the subject, the quantitative approach, to which he refers as ‘quantitative semantics,’ had a crucial influence on the birth of LL. And even though, at that time, it was given up for lack of ‘any logical justification’ (quoting the author), it contained rough versions of many concepts that were better understood, precisely introduced and developed much later, like differentiation and Taylor expansion for proofs. Around 2003, and thanks to the developments of LL and of the whole research area between logic and theoretical computer science, Ehrhard could come back to these fundamental intuitions and introduce the structure of finiteness space, allowing to reformulate this quantitative approach in a standard algebraic setting. The interpretation of LL in the category Fin of finiteness spaces and finitary relations suggested to Ehrhard and Regnier the differential extensions of LL and of the simply typed λ-calculus: Differential Linear Logic (DiLL) and the differential λ-calculus. The theory of LL proof-nets could be straightforwardly extended to DiLL, and a very natural notion of Taylor expansion of a proof-net (and of a λ-term) was introduced: an element of the Taylor expansion of the proof-net/term α is itself a (differential) proof-net/term and an approximation of α.
- Published
- 2018
7. 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
8. Glueability of Resource Proof-Structures: Inverting the Taylor Expansion
- Author
-
Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco, Guerrieri, Giulio, Pellissier, Luc, Tortora de Falco, Lorenzo, Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco, Guerrieri, Giulio, Pellissier, Luc, and Tortora de Falco, Lorenzo
- 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.
- Published
- 2020
- Full Text
- View/download PDF
9. Polarized and focalized linear and classical proofs
- Author
-
Laurent, Olivier, Quatrini, Myriam, and Tortora de Falco, Lorenzo
- Published
- 2005
- Full Text
- View/download PDF
10. Additives of linear logic and normalization—Part I: a (restricted) Church–Rosser property
- Author
-
Tortora de Falco, Lorenzo
- Published
- 2003
- Full Text
- View/download PDF
11. The additive multiboxes
- Author
-
Tortora de Falco, Lorenzo
- Published
- 2003
- Full Text
- View/download PDF
12. Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications
- Author
-
Ehrhard, Thomas, primary, Fernández, Maribel, additional, Paiva, Valeria de, additional, and Tortora de Falco, Lorenzo, additional
- Published
- 2019
- Full Text
- View/download PDF
13. 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
14. A semantic account of strong normalization in Linear Logic
- Author
-
de Carvalho Daniel, TORTORA DE FALCO, LORENZO, de Carvalho, Daniel, and TORTORA DE FALCO, Lorenzo
- 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.
- Published
- 2016
15. 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
16. Logica Volume 1- Dimostrazioni e modelli al primo ordine
- Author
-
ABRUSCI, Vito Michele, TORTORA DE FALCO, LORENZO, Abrusci, Vito Michele, and TORTORA DE FALCO, Lorenzo
- Published
- 2014
17. Computing Connected Proof(-Structure)s From Their Taylor Expansion
- Author
-
Guerrieri, Giulio, Pellissier, Luc, Tortora de Falco, Lorenzo, Guerrieri, Giulio, Pellissier, Luc, and Tortora de Falco, Lorenzo
- 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.
- Published
- 2016
- Full Text
- View/download PDF
18. Computing Connected Proof(-Structure)s From Their Taylor Expansion
- Author
-
Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco, Guerrieri, Giulio, Pellissier, Luc, Tortora de Falco, Lorenzo, Giulio Guerrieri and Luc Pellissier and Lorenzo Tortora de Falco, Guerrieri, Giulio, Pellissier, Luc, and Tortora de Falco, Lorenzo
- 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.
- Published
- 2016
- Full Text
- View/download PDF
19. Sulla struttura logica del calcolo
- Author
-
TORTORA DE FALCO, LORENZO and TORTORA DE FALCO, Lorenzo
- Abstract
Proponiamo una rassegna di alcuni aspetti degli sviluppi recenti della teoria della dimostrazione e dei suoi legami con l'informatica.
- Published
- 2006
20. Coherent obsessional experiments for linear logic proof-nets
- Author
-
TORTORA DE FALCO, LORENZO and TORTORA DE FALCO, Lorenzo
- Published
- 2001
21. Denotational semantics for polarized (but non-constrained) LK by means of the additives
- Author
-
TORTORA DE FALCO, LORENZO and TORTORA DE FALCO, Lorenzo
- Published
- 1997
22. Strong Normalization for all-style LK-tq
- Author
-
JOINET J. B, SCHELLINX H, TORTORA DE FALCO, LORENZO, JOINET J., B, Schellinx, H, and TORTORA DE FALCO, Lorenzo
- Published
- 1996
23. Polarisation des preuves classiques et renversement
- Author
-
TORTORA DE FALCO, LORENZO, QUATRINI M., TORTORA DE FALCO, Lorenzo, and Quatrini, M.
- Published
- 1996
24. Generalized standardization lemma for the additives
- Author
-
Tortora de Falco, Lorenzo, primary
- Published
- 1996
- Full Text
- View/download PDF
25. Generalized standardization lemma for the additives (preliminary report)
- Author
-
Tortora de Falco, Lorenzo
- 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.
- Full Text
- View/download PDF
26. Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
- Author
-
Guerrieri, Giulio, Pellissier, Luc, de Falco, Lorenzo Tortora, Guerrieri, Giulio, Pellissier, Luc, and TORTORA DE FALCO, Lorenzo
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,General Computer Science ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,FOS: Mathematics ,Mathematics - Logic ,Logic (math.LO) ,03F52, 03B47, 03B70 ,linear logic, Taylor expansion, proof-structure, pullback, natural transformation ,Logic in Computer Science (cs.LO) ,Theoretical Computer Science - 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 (and deciding in the finite case) 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. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.
- Published
- 2020
27. Taking Linear Logic Apart
- Author
-
Kokke, Wen, Montesi, Fabrizio, Peressotti, Marco, Ehrhard, Thomas, Fernández, Maribel, de Paiva, Valeria, and Tortora de Falco, Lorenzo
- Subjects
Process calculi ,Deadlock-freedom ,Logic ,Formal methods ,Linear logic ,Programming Languages ,Curry-Howard correspondence - Abstract
Process calculi based on logic, such as πDILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the π-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. [12] introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP − , a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP − supports the same communication protocols as CP.
- Published
- 2019
28. Proof-Net as Graph, Taylor Expansion as Pullback
- Author
-
Luc Pellissier, Lorenzo Tortora de Falco, Giulio Guerrieri, Giulio Guerrieri Luc Pellissier Lorenzo Tortora de Falco, Guerrieri, Giulio, Pellissier, Luc, Tortora de Falco, Lorenzo, Iemhoff, Rosalie, Moortgat, Michael, de Queiroz, Ruy, Department of Computer Science [Bath], University of Bath [Bath], Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Matematica [Roma TRE], Università degli Studi Roma Tre, and ANR-14-CE25-0007,RAPIDO,Raisonner et Programmer avec des Données Infinies(2014)
- Subjects
linear logic Proof-net Taylor expansion Graph ,Proof-net ,Linear logic ,0102 computer and information sciences ,01 natural sciences ,Graph ,Theoretical Computer Science ,symbols.namesake ,Taylor series ,0101 mathematics ,Mathematics ,Taylor expansion ,010102 general mathematics ,Multiplicative function ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Graph theory ,16. Peace & justice ,Exponential function ,Algebra ,010201 computation theory & mathematics ,symbols ,Proof net ,Computer Science(all) - Abstract
International audience; We introduce a new graphical representation for multiplica-tive 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.
- Published
- 2019
29. Preface
- Author
-
Thomas Ehrhard, Maribel Fernández, Valeria de Paiva, Lorenzo Tortora de Falco, Thomas Ehrhard, Maribel Fernández, Valeria de Paiva and Lorenzo Tortora de Falco, Ehrhard, Thoma, Fernández, Maribel, de Paiva, Valeria, and TORTORA DE FALCO, Lorenzo
- Published
- 2019
30. Logica
- Author
-
Vito Michele Abrusci, Lorenzo Tortora de Falco, Abrusci, Vito Michele, and TORTORA DE FALCO, Lorenzo
- Abstract
L'opera si propone come testo di riferimento per acquisire una solida preparazione specialistica nella Logica, presentando in maniera rigorosa ed innovativa argomenti tradizionalmente affrontati nei corsi universitari di secondo livello. Questo secondo volume, che completa l'opera, presenta le basi della teoria della ricorsività, l'aritmetica di Peano ed i teoremi di incompletezza, gli assiomi della teoria assiomatica degli insiemi di Zermelo-Fraenkel e la teoria degli ordinali e dei cardinali che ne deriva.
- Published
- 2018
31. An abstract approach to stratification in linear logic
- Author
-
Lorenzo Tortora de Falco, Pierre Boudes, Damiano Mazza, Boudes, Pierre, Mazza, Damiano, and TORTORA DE FALCO, Lorenzo
- Subjects
FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,Substructural logic ,Categorical logic ,LInear Logic ,Modal logic ,Higher-order logic ,Stratification (mathematics) ,Linear logic ,Logic in Computer Science (cs.LO) ,Computer Science Applications ,Theoretical Computer Science ,Algebra ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Computational Theory and Mathematics ,Linear temporal logic ,Computer Science::Logic in Computer Science ,Stratification ,03F52 ,Categorical variable ,Information Systems ,Mathematics - 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" subsystems), 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.
- Published
- 2015
32. A semantic measure of the execution time in linear logic
- Author
-
Michele Pagani, L. Tortora de Falco, Daniel de Carvalho, 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), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), ANR-07-BLAN-0324,CHOCO,Curry-Howard pour la concurrence(2007), DANIEL DE, Carvalho, Michele, Pagani, and TORTORA DE FALCO, Lorenzo
- Subjects
Denotational semantics ,Discrete mathematics ,Multiset ,Interpretation (logic) ,General Computer Science ,010102 general mathematics ,Linear logic ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,0102 computer and information sciences ,Net (mathematics) ,Linear Logic ,01 natural sciences ,Measure (mathematics) ,Theoretical Computer Science ,Computational complexity ,010201 computation theory & mathematics ,If and only if ,Kripke semantics ,0101 mathematics ,Denotational Semantic ,Computer Science(all) ,Mathematics - 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
- 2011
33. Strong normalization property for second order linear logic
- Author
-
Lorenzo Tortora de Falco, Michele Pagani, 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), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Pagani, M, and TORTORA DE FALCO, Lorenzo
- Subjects
Normalization (statistics) ,Normalization property ,Correctness ,General Computer Science ,Linear logic ,0102 computer and information sciences ,01 natural sciences ,Linear ordering ,Theoretical Computer Science ,Proof-nets ,(Weak, strong) normalization ,(weakstrong)normalization ,0101 mathematics ,Mathematics ,proof-nets ,Discrete mathematics ,010102 general mathematics ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Sliced pure structures ,Confluence ,16. Peace & justice ,Standardization ,010201 computation theory & mathematics ,confluence ,Additive connectives ,Algorithm ,Computer Science(all) - Abstract
International audience; 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 our 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.
- Published
- 2010
34. Obsessional experiments for linear logic proof-nets
- Author
-
Lorenzo Tortora de Falco and TORTORA DE FALCO, Lorenzo
- Subjects
Discrete mathematics ,Algebra ,Geometry of interaction ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Mathematics (miscellaneous) ,Semantics (computer science) ,Computer science ,Higher-order logic ,Injective function ,Linear logic ,Computer Science Applications - Abstract
We address the question of injectivity of coherent semantics of linear logic proof-nets. Starting from Girard's definition of experiment, we introduce the key-notion of ‘injective obsessional experiment’, which allows us 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.
- Published
- 2003
35. The additive multiboxes
- Author
-
Lorenzo Tortora de Falco and TORTORA DE FALCO, Lorenzo
- Subjects
Geometry of interaction ,Discrete mathematics ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Logic ,Multiplicative function ,Linear logic ,Mathematics - 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.
- Published
- 2003
- Full Text
- View/download PDF
36. The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)
- Author
-
Daniel de Carvalho, Lorenzo Tortora de Falco, DE CARVALHO, D, and TORTORA DE FALCO, Lorenzo
- Subjects
Discrete mathematics ,FOS: Computer and information sciences ,Denotational semantics ,Multiset ,Computer Science - Logic in Computer Science ,Interpretation (logic) ,Logic ,Multiplicative function ,Linear logic ,Injective function ,Logic in Computer Science (cs.LO) ,Proof-nets ,Fragment (logic) ,Computer Science::Logic in Computer Science ,Relational model ,Equivalence relation ,Computer Science::Programming Languages ,Injective model ,Mathematics - Abstract
We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides 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. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponential boxes"., 36 pages
- Published
- 2010
37. 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
38. 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
39. Generalized Standardization lemma for the additives
- Author
-
Lorenzo Tortora de Falco and TORTORA DE FALCO, Lorenzo
- Subjects
TheoryofComputation_MISCELLANEOUS ,Lemma (mathematics) ,Pure mathematics ,General Computer Science ,Standardization ,Preliminary report ,Confluence ,Commutative property ,Linear logic ,Mathematics ,Theoretical Computer Science ,Computer Science(all) - 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.
- Published
- 1996
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.