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

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

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)

Cited In (21)

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

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)