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

DOI10.1016/J.APAL.2011.09.012zbMATH Open1239.03040OpenAlexW1966461321MaRDI QIDQ408540FDOQ408540

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

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

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)

Cites Work

• Linear logic
• Light types for polynomial time computation in lambda calculus
• Bounded linear logic: A modular approach to polynomial-time computability
• Light linear logic
• Soft linear logic and polynomial time
• Intuitionistic light affine logic
• On the computational complexity of cut-elimination in linear logic.
• Title not available (Why is that?)
• Phase semantics for light linear logic
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (9)

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

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)