Realizability models for a linear dependent PCF

DOI10.1016/j.tcs.2015.03.005zbMath1327.68109MaRDI QIDQ2346992

Aloïs Brunel, Marco Gaboardi

Publication date: 26 May 2015

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

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

zbMATH Keywords

implicit computational complexity; realizability model

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q15: Complexity classes (hierarchies, relations among complexity classes, etc.)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Realizability models and implicit complexity
• Computational ludics
• Bounded linear logic: A modular approach to polynomial-time computability
• A new recursion-theoretic characterization of the polytime functions
• Realizability models for BLL-like languages
• Quantitative classical realizability
• Locus Solum: From the rules of logic to the logic of rules
• Biorthogonality, step-indexing and compiler correctness
• Resource control graphs
• Extending Type Theory with Forcing
• Realizability algebras: a program to well order R
• Realisability semantics of parametric polymorphism, general references and recursive types
• Parametric polymorphism and operational equivalence
• Linear Dependent Types and Relative Completeness
• Dependent ML An approach to practical programming with dependent types
• Bounded Linear Logic, Revisited