Realizability models and implicit complexity

DOI10.1016/j.tcs.2010.12.025zbMath1222.03065OpenAlexW1989703373MaRDI QIDQ534712

Ugo Dal Lago, Martin Hofmann

Publication date: 10 May 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.025

zbMATH Keywords

modalitypolymorphismlinear logicrealizabilityimplicit computational complexityinductive datatypes

Mathematics Subject Classification ID

Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (7)

Higher-order interpretations and program complexity ⋮ Probabilistic Termination by Monadic Affine Sized Typing ⋮ Unnamed Item ⋮ Quantitative classical realizability ⋮ Realizability models for a linear dependent PCF ⋮ Implicit computation complexity in higher-order programming languages ⋮ A quantitative model for simply typed λ-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functional interpretations of feasibly constructive arithmetic
• The weak lambda calculus as a reasonable machine
• A semantic proof of polytime soundness of light affine logic
• A small complete category
• Light linear logic
• Linear types and non-size-increasing polynomial time computation.
• 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
• Foundations of Software Science and Computation Structures
• Intuitionistic Light Affine Logic
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science

This page was built for publication: Realizability models and implicit complexity