Light linear logics with controlled weakening: expressibility, confluent strong normalization

DOI10.1016/j.apal.2011.09.012zbMath1239.03040OpenAlexW1966461321MaRDI QIDQ408540

Max I. Kanovich

Publication date: 10 April 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2011.09.012

zbMATH Keywords

implicit computational complexityelementary linear logiclight linear logicpolynomial-time strong normalizationproofs-as-programs paradigm

Mathematics Subject Classification ID

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

Related Items

Soft subexponentials and multiplexing

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Light types for polynomial time computation in lambda calculus
• Bounded linear logic: A modular approach to polynomial-time computability
• Light linear logic
• Phase semantics for light linear logic
• Soft linear logic and polynomial time
• On an interpretation of safe recursion in light affine logic
• Linear logic and polynomial time
• Light Linear Logic with Controlled Weakening
• Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic
• Intuitionistic Light Affine Logic
• Theoretical Computer Science