A semantic proof of polytime soundness of light affine logic

DOI10.1007/s00224-009-9210-xzbMath1205.68169OpenAlexW1967535898MaRDI QIDQ987375

Martin Hofmann, Ugo Dal Lago

Publication date: 13 August 2010

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00224-009-9210-x

zbMATH Keywords

linear logicrealizabilityimplicit computational complexity

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (4)

Realizability models and implicit complexity ⋮ Quantitative classical realizability ⋮ Implicit computation complexity in higher-order programming languages ⋮ A quantitative model for simply typed λ-calculus

Cites Work

• Phase semantics and decidability of elementary affine logic
• Functional interpretations of feasibly constructive arithmetic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The weak lambda calculus as a reasonable machine
• Light linear logic
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• Realizability models for BLL-like languages
• Soft linear logic and polynomial time
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A semantic proof of polytime soundness of light affine logic