Bounded linear logic: A modular approach to polynomial-time computability
From MaRDI portal
Publication:1193854
DOI10.1016/0304-3975(92)90386-TzbMath0788.03005OpenAlexW1971256104WikidataQ126351278 ScholiaQ126351278MaRDI QIDQ1193854
Jean-Yves Girard, Andrej Scedrov, Philip J. Scott
Publication date: 27 September 1992
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(92)90386-t
polynomial-time algorithmcomplexity specificationspolynomial-time functionrestricted version of linear logic
Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items (57)
Computation by interaction for space-bounded functional programming ⋮ Modular Inference of Linear Types for Multiplicity-Annotated Arrows ⋮ Holomorphic models of exponential types in linear logic ⋮ Cut elimination for the unified logic ⋮ Linear Dependent Type Theory for Quantum Programming Languages ⋮ Semantics of weakening and contraction ⋮ The complexity of Horn fragments of linear logic ⋮ A new “feasible” arithmetic ⋮ Paths-based criteria and application to linear logic subsystems characterizing polynomial time ⋮ Petri nets, Horn programs, linear logic and vector games ⋮ Normal functors, power series and \(\lambda\)-calculus ⋮ Phase semantics and decidability of elementary affine logic ⋮ Linear logic automata ⋮ A linear conservative extension of Zermelo-Fraenkel set theory ⋮ Light affine lambda calculus and polynomial time strong normalization ⋮ Natural deduction and coherence for weakly distributive categories ⋮ New Curry-Howard terms for full linear logic ⋮ Expressing computational complexity in constructive type theory ⋮ A Characterization of NC k by First Order Functional Programs ⋮ Simple free star-autonomous categories and full coherence ⋮ Light linear logics with controlled weakening: expressibility, confluent strong normalization ⋮ Phase semantics for light linear logic ⋮ Sound approximate and asymptotic probabilistic bisimulations for PCTL ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ Linearity and uniqueness: an entente cordiale ⋮ The syntactic side of autonomous categories enriched over generalised metric spaces ⋮ On quantum lambda calculi: a foundational perspective ⋮ Build your own clarithmetic I: Setup and completeness ⋮ Introduction to clarithmetic. I ⋮ Linear dependent types in a call-by-value scenario ⋮ Unnamed Item ⋮ Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials ⋮ Quantum coherent spaces and linear logic ⋮ Generalized bounded linear logic and its categorical semantics ⋮ Graded modal dependent type theory ⋮ Soft linear set theory ⋮ Decision problems for propositional linear logic ⋮ Bounded linear logic: A modular approach to polynomial-time computability ⋮ Light linear logic ⋮ Gödel's system \(\mathcal T\) revisited ⋮ Syllogisms in rudimentary linear logic, diagrammatically ⋮ Linearizing intuitionistic implication ⋮ Taming Modal Impredicativity: Superlazy Reduction ⋮ Light Linear Logic with Controlled Weakening ⋮ Unnamed Item ⋮ Bounded Linear Logic, Revisited ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Light linear logic ⋮ Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic ⋮ Realizability models for BLL-like languages ⋮ Soft linear logic and polynomial time ⋮ Unnamed Item ⋮ Linear logic by levels and bounded time complexity ⋮ An abstract approach to stratification in linear logic ⋮ Realizability models for a linear dependent PCF ⋮ Implicit computation complexity in higher-order programming languages ⋮ Resourceful program synthesis from graded linear types
Cites Work
- Linear logic
- Computational interpretations of linear logic
- Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
- Bounded linear logic: A modular approach to polynomial-time computability
- The structure of multiplicatives
- Relational queries computable in polynomial time
- Π12-logic, Part 1: Dilators
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Bounded linear logic: A modular approach to polynomial-time computability
