Realizability models for BLL-like languages

DOI10.1016/j.tcs.2003.10.019zbMath1047.03049OpenAlexW1979524717MaRDI QIDQ1827395

Martin Hofmann, Philip J. Scott

Publication date: 6 August 2004

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

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

zbMATH Keywords

Linear logicFinite model theoryComplexity lambda calculus

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Model theory of finite structures (03C13) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Complexity of proofs (03F20) Descriptive complexity and finite models (68Q19)

Related Items (8)

Generalized bounded linear logic and its categorical semantics ⋮ Realizability models and implicit complexity ⋮ A semantic proof of polytime soundness of light affine logic ⋮ Bounded Linear Logic, Revisited ⋮ Aspects of Categorical Recursion Theory ⋮ Quantitative classical realizability ⋮ Realizability models for a linear dependent PCF ⋮ Implicit computation complexity in higher-order programming languages

Cites Work

• A small complete category
• Characterizing complexity classes by higher type primitive recursive definitions
• Bounded linear logic: A modular approach to polynomial-time computability
• Light linear logic
• Phase semantics for light linear logic
• Linear types and non-size-increasing polynomial time computation.
• Safe recursion with higher types and BCK-algebra
• Stratified coherence spaces: A denotational semantics for light linear logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Realizability models for BLL-like languages