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

DOI10.1016/J.APAL.2011.09.012MaRDI QIDQ408540zbMATH OpenOpenAlexFDO

Authors Max 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

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

Recommendations

• Light Linear Logic with Controlled Weakening
• Linear logic and polynomial time
• Light linear logic
• Light affine lambda calculus and polynomial time strong normalization
• Linear logic by levels and bounded time complexity

Cites work

• scientific article; zbMATH DE number 786485 (Why is no real title available?)
• scientific article; zbMATH DE number 1392281 (Why is no real title available?)
• scientific article; zbMATH DE number 1424054 (Why is no real title available?)
• Bounded linear logic: A modular approach to polynomial-time computability
• Intuitionistic light affine logic
• Light Linear Logic with Controlled Weakening
• Light linear logic
• Light types for polynomial time computation in lambda calculus
• Linear logic
• Linear logic and polynomial time
• On an interpretation of safe recursion in light affine logic
• On the computational complexity of cut-elimination in linear logic.
• Phase semantics for light linear logic
• Soft linear logic and polynomial time
• Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic

Cited in

(9)

• Free-cut elimination in linear logic and an application to a feasible arithmetic
• On the computational complexity of cut-elimination in linear logic.
• Soft subexponentials and multiplexing
• Linear logic by levels and bounded time complexity
• Linear logic and polynomial time
• Light Linear Logic with Controlled Weakening
• Parallelism in soft linear logic
• An abstract approach to stratification in linear logic
• Paths-based criteria and application to linear logic subsystems characterizing polynomial time

This page was built for publication: Light linear logics with controlled weakening: expressibility, confluent strong normalization

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