Bounded linear logic: A modular approach to polynomial-time computability

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

zbMATH Keywords

polynomial-time algorithm complexity specifications polynomial-time function restricted version of linear logic

Mathematics Subject Classification ID

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

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, 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