The Experts below are selected from a list of 61524 Experts worldwide ranked by ideXlab platform
Martin Hofmann - One of the best experts on this subject based on the ideXlab platform.
-
Bounded Linear Logic, Revisited
Logical Methods in Computer Science, 2010Co-Authors: Ugo Dal Lago, Martin HofmannAbstract:We present QBAL, an extension of Girard, Scedrov and Scott's bounded Linear Logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded Linear Logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
-
Type inference in intuitionistic Linear Logic
2010Co-Authors: Patrick Baillot, Martin HofmannAbstract:We study the type checking and type inference problems for intuitionistic Linear Logic: given a System F typed -term, (i) for an alleged Linear Logic type, determine whether there exists a corresponding typing derivation in Linear Logic (type checking) (ii) provide a concise description of all possible corresponding Linear Logic typings (type inference). We solve these problems using a novel algorithmic type system for Linear Logic whose typing rules carry arithmetic side conditions describing essentially the nesting depth of (proof-net) boxes. By understanding these side conditions as unknowns we then reduce type inference to solving a system of arithmetic constraints. We show that these constraint systems fall into a tractable class hence leading to an efficient (polynomial-time) solution. There are two important restrictions: first, our source language is typed System F rather than untyped lambda calculus; this is necessary because type inference for System F is known to be undecidable. Second, we assume that sharing is made explicit in the input, thus we do not try to automatically infer opportunities for sharing identical subterms. Relieving the latter restriction is left as a challenge for future work.
-
PPDP - Type inference in intuitionistic Linear Logic
Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming - PPDP '10, 2010Co-Authors: Patrick Baillot, Martin HofmannAbstract:International audienceWe study the type checking and type inference problems for intuitionistic Linear Logic: given a System F typed -term, (i) for an alleged Linear Logic type, determine whether there exists a corresponding typing derivation in Linear Logic (type checking) (ii) provide a concise description of all possible corresponding Linear Logic typings (type inference). We solve these problems using a novel algorithmic type system for Linear Logic whose typing rules carry arithmetic side conditions describing essentially the nesting depth of (proof-net) boxes. By understanding these side conditions as unknowns we then reduce type inference to solving a system of arithmetic constraints. We show that these constraint systems fall into a tractable class hence leading to an efficient (polynomial-time) solution. There are two important restrictions: first, our source language is typed System F rather than untyped lambda calculus; this is necessary because type inference for System F is known to be undecidable. Second, we assume that sharing is made explicit in the input, thus we do not try to automatically infer opportunities for sharing identical subterms. Relieving the latter restriction is left as a challenge for future work
-
TLCA - Bounded Linear Logic, Revisited
Lecture Notes in Computer Science, 2009Co-Authors: Ugo Dal Lago, Martin HofmannAbstract:We present QBAL, an extension of Girard, Scedrov and Scott's bounded Linear Logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded Linear Logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
Ugo Dal Lago - One of the best experts on this subject based on the ideXlab platform.
-
Bounded Linear Logic, Revisited
Logical Methods in Computer Science, 2010Co-Authors: Ugo Dal Lago, Martin HofmannAbstract:We present QBAL, an extension of Girard, Scedrov and Scott's bounded Linear Logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded Linear Logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
-
Context semantics, Linear Logic, and computational complexity
ACM Transactions on Computational Logic, 2009Co-Authors: Ugo Dal LagoAbstract:We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in Linear Logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the amount of resources needed to compute the normal form. Weights are then exploited in proving strong soundness theorems for various subsystems of Linear Logic, namely elementary Linear Logic, soft Linear Logic, and light Linear Logic.
-
TLCA - Bounded Linear Logic, Revisited
Lecture Notes in Computer Science, 2009Co-Authors: Ugo Dal Lago, Martin HofmannAbstract:We present QBAL, an extension of Girard, Scedrov and Scott's bounded Linear Logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded Linear Logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
-
Context Semantics, Linear Logic and Computational Complexity
arXiv: Logic in Computer Science, 2005Co-Authors: Ugo Dal LagoAbstract:We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in Linear Logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of Linear Logic, namely elementary Linear Logic, soft Linear Logic and light Linear Logic.
-
LICS - Context Semantics, Linear Logic and Computational Complexity
21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), 1Co-Authors: Ugo Dal LagoAbstract:We show that context semantics can be fruitfully applied to the quantitative analysis of proof normalization in Linear Logic. In particular, context semantics lets us define the weight of a proof-net as a measure of its inherent complexity: it is both an upper bound to normalization time (modulo a polynomial overhead, independently on the reduction strategy) and a lower bound to the number of steps to normal form (for certain reduction strategies). Weights are then exploited in proving strong soundness theorems for various subsystems of Linear Logic, namely elementary Linear Logic, soft Linear Logic and light Linear Logic.
Max I. Kanovich - One of the best experts on this subject based on the ideXlab platform.
-
Simulating Linear Logic in 1-Only Linear Logic
arXiv: Logic in Computer Science, 2017Co-Authors: Max I. KanovichAbstract:Linear Logic was introduced by Girard as a resource-sensitive refinement of classical Logic. It turned out that full propositional Linear Logic is undecidable (Lincoln, Mitchell, Scedrov, and Shankar) and, hence, it is more expressive than (modalized) classical or intuitionistic Logic. In this paper we focus on the study of the simplest fragments of Linear Logic, such as the one-literal and constant-only fragments (the latter contains no literals at all). Here we demonstrate that all these extremely simple fragments of Linear Logic (one-literal, $\bot$-only, and even unit-only) are exactly of the same expressive power as the corresponding full versions. We present also a complete computational interpretation (in terms of acyclic programs with stack) for bottom-free Intuitionistic Linear Logic. Based on this interpretation, we prove the fairness of our encodings and establish the foregoing complexity results.
-
Phase semantics for light Linear Logic
Theoretical Computer Science, 2003Co-Authors: Max I. Kanovich, Mitsuhiro Okada, Andre ScedrovAbstract:Light Linear Logic (Girard, Inform. Comput. 14 (1998) 175-204) is a refinement of the propositions-as-types paradigm to polynomial-time computation. A semantic setting for the underlying Logical system is introduced here in terms of fibred phase spaces. Strong completeness is established, with a purely semantic proof of cut elimination as a consequence. A number of mathematical examples of fibred phase spaces are presented that illustrate subtleties of light Linear Logic.
-
Linear Logic automata
Annals of Pure and Applied Logic, 1996Co-Authors: Max I. KanovichAbstract:Abstract A Linear Logic automaton is a hybrid of a finite automaton and a non-deterministic Petri net. LL automata commands are represented by propositional Horn Linear Logic formulas. Computations performed by LL automata directly correspond to cut-free derivations in Linear Logic. A programming language of LL automata is developed in which typical sequential, non-deterministic and parallel programming constructs are expressed in the natural way. All non-deterministic computations, e.g. computations performed by programs built up of guarded commands in the Dijkstra's approach to non-deterministic programming, are directly simulated within the framework of Linear Logic automata, and thereby within the Horn framework of Linear Logic.
-
The complexity of Horn fragments of Linear Logic
Annals of Pure and Applied Logic, 1994Co-Authors: Max I. KanovichAbstract:Abstract The question at issue is to develop a computational interpretation of Girard's Linear Logic [Girard, 1987] and to obtain efficient decision algorithms for this Logic, based on the bottom-up approach . It involves starting with the simplest natural fragment of Linear Logic and then expanding it step-by-step. We give a complete computational interpretation for the Horn fragment of Linear Logic and some natural generalizations of it enriched by the two additive connectives: ⊛ and &. Within the framework of this interpretation, it becomes possible to explicitly formalize and clarify the computational aspects of the fragments of Linear Logic in question and establish exactly the complexity level of these fragments. In particular, the simplest natural Horn fragment of Linear Logic is proved to be NP-complete. As a corollary, we obtain the affirmative solution for the problem (formulated by Lincoln et al. (1992)): whether the multiplicative fragment of Linear Logic is NP-complete.
-
Linear Logic as a Logic of computations
Annals of Pure and Applied Logic, 1994Co-Authors: Max I. KanovichAbstract:Abstract The question at issue is to develop a computational interpretation of Linear Logic [8] and to establish exactly its expressive power. We follow the bottom-up approach. This involves starting with the simplest of the systems we are interested in, and then expanding them step-by-step. We begin with the !-Horn fragment of Linear Logic, which uses only positive literals, the Linear implication ⊸, the tensor product ⊗, and the modal storage operator !. We give a complete computational interpretation for the !-Horn fragment of Linear Logic and for some natural generalizations of it formed by introducing additive connectives. Here we use the well-known ‘or’-like connective ⊕, and, for the sake of the computational duality, we introduce a new ‘and’-like connective @ For !-Horn sequents, we prove that their derivability problem is directly equivalent to the reachability problem for Petri nets, which is known to be decidable [19]. For the (!, ⊕)-Horn fragment of Linear Logic, which uses only positive literals, the Linear implication ⊸, the tensor product ⊗, the modal storage operator!, and the additive ‘disjunction’ ⊕, we prove that standard Minsky machines [21] can be directly encoded in this (!, ⊕)-Horn fragment. Standard Minsky machines can be directly encoded in the corresponding ‘dual’ (!, @)-Horn fragment of Linear Logic, as well. As a corollary, both these fragments of Linear Logic are proved to be undecidable.
Mati Pentus - One of the best experts on this subject based on the ideXlab platform.
-
LFCS - Equivalence of Multiplicative Fragments of Cyclic Linear Logic and Noncommutative Linear Logic
Logical Foundations of Computer Science, 1997Co-Authors: Mati PentusAbstract:In this paper we consider two associative noncommutative analogs of Girard's Linear Logic. These are Abrusci's noncommutative Linear Logic and Yetter's cyclic Linear Logic.
Kaustuv Chaudhuri - One of the best experts on this subject based on the ideXlab platform.
-
Hybrid Linear Logic, revisited
Mathematical Structures in Computer Science, 2019Co-Authors: Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte, Elaine PimentelAbstract:HyLL (Hybrid Linear Logic) is an extension of intuitionistic Linear Logic (ILL) that has been used as a framework for specifying systems that exhibit certain modalities. In HyLL, truth judgements are labelled by worlds (having a monoidal structure) and hybrid connectives ( at and ↓) relate worlds with formulas. We start this work by showing that HyLL's axioms and rules can be adequately encoded in Linear Logic (LL), so that one focused step in LL will correspond to a step of derivation in HyLL. This shows that any proof in HyLL can be exactly mimicked by a LL focused derivation. Another extension of LL that has extensively been used for specifying systems with modalities is Subexponential Linear Logic (SELL). In SELL, the LL exponentials (!, ?) are decorated with labels representing locations , and a pre-order on such labels defines the provability relation. We propose an encoding of HyLL into SELL ⋒ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. More precisely, we identify worlds as locations, and show that a flat subexponential structure is sufficient for representing any world structure in HyLL. This shows that HyLL's monoidal structure is not reflected in LL derivations, hence not increasing the expressiveness of LL, from a proof theoretical point of view. We conclude by proposing the notion of fixed points in multiplicative additive HyLL (μHyMALL), which can be encoded into multiplicative additive Linear Logic with fixed points (μMALL). As an application, we propose encodings of Computational Tree Logic (CTL) into both μMALL and μHyMALL. In the former, states are represented as atoms in the Linear context, hence reflecting a more operational view of CTL connectives. In the latter, worlds represent states of the transition system, thus exhibiting a pleasant similarity with the semantics of CTL.
-
A judgmental analysis of Linear Logic
2018Co-Authors: Bor-yuh Evan Chang, Kaustuv Chaudhuri, Frank PfenningAbstract:We reexamine the foundations of Linear Logic, developing a system of natural deduction following Martin-Löf’s separation of judgments from propositions. Our construction yields a clean and elegant formulation that accounts for a rich set of multiplicative, additive, and exponential connectives, extending dual intuitionistic Linear Logic but differing from both classical Linear Logic and Hyland and de Paiva’s full intuitionistic Linear Logic. We also provide a corresponding sequent calculus that admits a simple proof of the admissibility of cut by a single structural induction. Finally, we show how to interpret classical Linear Logic (with or without the MIX rule) in our system, employing a form of double-negation translation
-
The focused inverse method for Linear Logic
2006Co-Authors: Frank Pfenning, Kaustuv ChaudhuriAbstract:Linear Logic presents a unified framework for describing and reasoning about stateful systems. Because of its view of hypotheses as resources, it supports such phenomena as concurrency, external and internal choice, and state transitions that are common in such domains as protocol verification, concurrent computation, process calculi and games. It accomplishes this unifying view by providing Logical connectives whose behaviour is closely tied to the precise collection of resources. The interaction of the rules for multiplicative, additive and exponential connectives gives rise to a wide and expressive array of behaviours. This expressivity comes with a price: even simple fragments of the Logic are highly complex or undecidable. Various approaches have been taken to produce automated reasoning systems for fragments of Linear Logic. This thesis addresses the need for automated reasoning for the complete set of connectives for first-order intuitionistic Linear Logic (⊗, 1, m , &, t , ⊕, 0, !, ∀, ∃), which removes the need for any idiomatic constructions in smaller fragments and instead allows direct Logical expression. The particular theorem proving technique used is a novel combination of a variant of Maslov's inverse method using Andreoli's focused derivations in the sequent calculus as the underlying framework. The goal of this thesis is to establish the focused inverse method as the premier means of automated reasoning in Linear Logic. To this end, the technical claims are substantiated with an implementation of a competitive first-order theorem prover for Linear Logic---as of this writing, the only one of its kind.
-
Resource Management for the Inverse Method in Linear Logic
2003Co-Authors: Kaustuv Chaudhuri, Frank PfenningAbstract:One central aspect of proof search in Linear Logic is resource management. Strategies for efficient resource management have been de- veloped for backward-directed calculi, such as top-down Linear Logic pro- gramming, tableaux calculi, and matrix methods. In this paper we con- sider resource management for forward-directed calculi, such as the in- verse method, clausal resolution, and bottom-up Linear Logic program- ming. We focus on the inverse method for intuitionistic Linear Logic, and isolate the resource management problems. They turn out to come from exponentials, additive unit, and multiplicative unit, exhibiting some sur- prising differences from the backward-directed calculi. Our solution em- ploys controlled contraction and weakening, and introduces affine hy- potheses into sequents. In Linear Logic (5,2), hypotheses are viewed as resources, with the number of oc- currences playing a central role in the proof theory. This property allows natural encodings of theories that are difficult to express in the standard Logic. Theorem proving in Linear Logic has an additional component of resource management which is not as critical for the standard Logic. The kinds of these resource man- agement problems are determined by the direction in which inference rules are read:
