Linear logic and elementary time

DOI10.1016/S0890-5401(03)00010-5zbMath1019.03039OpenAlexW2106173595MaRDI QIDQ1401946

Vincent Danos, Jean-Baptiste Joinet

Publication date: 19 August 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0890-5401(03)00010-5

zbMATH Keywords

elementary recursive functionselementary linear logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Logarithmic space and permutations, Bounded combinatory logic and lower complexity, Paths-based criteria and application to linear logic subsystems characterizing polynomial time, Characterizing polynomial and exponential complexity classes in elementary lambda-calculus, On Paths-Based Criteria for Polynomial Time Complexity in Proof-Nets, Phase semantics and decidability of elementary affine logic, Light affine lambda calculus and polynomial time strong normalization, A type-assignment of linear erasure and duplication, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, 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, Characterizingco-NLby a group action, Type inference for light affine logic via constraints on words, Unnamed Item, Unnamed Item, Unnamed Item, Unary Resolution: Characterizing Ptime, Unnamed Item, Bounded Linear Logic, Revisited, Stratified coherence spaces: A denotational semantics for light linear logic, Linear logic by levels and bounded time complexity, Proofs, Reasoning and the Metamorphosis of Logic, On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy, The additive multiboxes, Implicit computation complexity in higher-order programming languages

Cites Work

• Linear logic
• Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
• Stratified coherence spaces: A denotational semantics for light linear logic
• A new constructive logic: classic logic
• A new deconstructive logic: linear logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item