On the computational complexity of cut-elimination in linear logic.

DOI10.1007/B13810zbMATH Open1257.03091OpenAlexW3144329707MaRDI QIDQ5897348FDOQ5897348

Authors Kazushige Terui, Harry G. Mairson 

Publication date 23 February 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b13810

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of computation (including implicit computational complexity) (03D15)

Recommendations

• Decision problems for propositional linear logic
• scientific article; zbMATH DE number 785051
• Light linear logics with controlled weakening: expressibility, confluent strong normalization
• Light linear logic
• Linear logic and polynomial time

Cited in

(22)

• Free-cut elimination in linear logic and an application to a feasible arithmetic
• The role of polymorphism in the characterisation of complexity by soft types
• MALL proof equivalence is logspace-complete, via binary decision diagrams
• Cut elimination in multifocused linear logic
• Complexity bounds for sum-product logic via additive proof nets and Petri nets
• Linear additives
• Linear logic by levels and bounded time complexity
• Encodings of Turing machines in linear logic
• Implicit computation complexity in higher-order programming languages
• Polynomial time in untyped elementary linear logic
• Light linear logics with controlled weakening: expressibility, confluent strong normalization
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Computer Science Logic
• On paths-based criteria for polynomial time complexity in proof-nets
• Light affine lambda calculus and polynomial time strong normalization
• Light Linear Logic with Controlled Weakening
• A type-assignment of linear erasure and duplication
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• A By-Level Analysis of Multiplicative Exponential Linear Logic
• Sufficient conditions for cut elimination with complexity analysis
• scientific article; zbMATH DE number 2020177 (Why is no real title available?)
• FUNCTIONAL PEARL Linear lambda calculus and PTIME-completeness

This page was built for publication: On the computational complexity of cut-elimination in linear logic.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5897348)