Light linear logic
From MaRDI portal
Publication:1271560
DOI10.1006/inco.1998.2700zbMath0912.03025OpenAlexW1969548989MaRDI QIDQ1271560
Publication date: 3 May 1999
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/6dba9476865a8bf6fdc51d8660fde45b10dc4df0
naive set theoryproof-netspolytime functionscomplexity of cut-eliminationElementary Linear Logicexponentials of Linear Logicexpressive power of a logical systemfunctions representable in a logical systemLight Linear Logiclogical approach to complexity
Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20) Complexity of proofs (03F20)
Related Items (82)
Two function algebras defining functions in \(\mathsf{NC}^k\) Boolean circuits ⋮ The role of polymorphism in the characterisation of complexity by soft types ⋮ A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization ⋮ Bounded combinatory logic and lower complexity ⋮ Linear Logic Properly Displayed ⋮ A linear logic framework for multimodal logics ⋮ (Optimal) duplication is not elementary recursive ⋮ A new “feasible” arithmetic ⋮ A Short Introduction to Implicit Computational Complexity ⋮ Parsimonious Types and Non-uniform Computation ⋮ Implementing Cantor’s Paradise ⋮ Paths-based criteria and application to linear logic subsystems characterizing polynomial time ⋮ Characterizing polynomial and exponential complexity classes in elementary lambda-calculus ⋮ A type-based complexity analysis of object oriented programs ⋮ On quasi-interpretations, blind abstractions and implicit complexity ⋮ A By-Level Analysis of Multiplicative Exponential Linear Logic ⋮ On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets ⋮ Stability and paradox in algorithmic logic ⋮ Phase semantics and decidability of elementary affine logic ⋮ Light affine lambda calculus and polynomial time strong normalization ⋮ Jump from parallel to sequential proofs: exponentials ⋮ Computational Complexity Via Finite Types ⋮ A Characterization of NC k by First Order Functional Programs ⋮ Light linear logics with controlled weakening: expressibility, confluent strong normalization ⋮ Additives of linear logic and normalization. I: A (restricted) Church-Rosser property. ⋮ Phase semantics for light linear logic ⋮ Read/write factorizable programs ⋮ Linear types and non-size-increasing polynomial time computation. ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Light logics and optimal reduction: completeness and complexity ⋮ Complete and tractable machine-independent characterizations of second-order polytime ⋮ A proof-theoretic investigation of a logic of positions ⋮ Light logics and higher-order processes ⋮ Infinitary action logic with multiplexing ⋮ Build your own clarithmetic I: Setup and completeness ⋮ Introduction to clarithmetic. I ⋮ Recursion Schemata for NC k ⋮ Encodings of Turing machines in linear logic ⋮ Cofree coalgebras and differential linear logic ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ Soft linear set theory ⋮ Manipulating Sources of Information: Towards an Interpretation of Linear Logic and Strong Relevance Logic ⋮ Controlling Program Extraction in Light Logics ⋮ An Elementary Affine λ-Calculus with Multithreading and Side Effects ⋮ Combining linear logic and size types for implicit complexity ⋮ Polynomial time in untyped elementary linear logic ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Preface to the special volume ⋮ A semantic measure of the execution time in linear logic ⋮ Realizability models and implicit complexity ⋮ Type inference for light affine logic via constraints on words ⋮ Unnamed Item ⋮ Structural recursion as a query language on lists and ordered trees ⋮ An arithmetic for polynomial-time computation ⋮ A semantic proof of polytime soundness of light affine logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Taming Modal Impredicativity: Superlazy Reduction ⋮ Light Linear Logic with Controlled Weakening ⋮ Plugging-in proof development environments usingLocksinLF ⋮ Polynomial time over the reals with parsimony ⋮ Light types for polynomial time computation in lambda calculus ⋮ MODAL LOGIC WITHOUT CONTRACTION IN A METATHEORY WITHOUT CONTRACTION ⋮ Bounded Linear Logic, Revisited ⋮ Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets ⋮ Stratified coherence spaces: A denotational semantics for light linear logic ⋮ Realizability models for BLL-like languages ⋮ Soft linear logic and polynomial time ⋮ On an interpretation of safe recursion in light affine logic ⋮ Higher type recursion, ramification and polynomial time ⋮ Is the Optimal Implementation Inefficient? Elementarily Not ⋮ Quantum implicit computational complexity ⋮ Linear logic by levels and bounded time complexity ⋮ Focussing and proof construction ⋮ Enhancing induction in a contraction free logic with unrestricted abstraction: from \(\mathbf{Z}\) to \(\mathbf{Z}_2\) ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Proofs, Reasoning and the Metamorphosis of Logic ⋮ Soft subexponentials and multiplexing ⋮ On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy ⋮ An abstract approach to stratification in linear logic ⋮ The additive multiboxes ⋮ Implicit computation complexity in higher-order programming languages
Cites Work
This page was built for publication: Light linear logic
