Safe recursion with higher types and BCK-algebra

DOI10.1016/S0168-0072(00)00010-5zbMath0959.68075MaRDI QIDQ1577481

Martin Hofmann

Publication date: 4 September 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

Bellantoni-Cook's function algebra

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

06F35: BCK-algebras, BCI-algebras

68Q55: Semantics in the theory of computing

03D15: Complexity of computation (including implicit computational complexity)

03D65: Higher-type and set recursion theory

Related Items

A new “feasible” arithmetic, A Calculus for Game-Based Security Proofs, Type inference for light affine logic via constraints on words, Light affine lambda calculus and polynomial time strong normalization, A semantic proof of polytime soundness of light affine logic, Light types for polynomial time computation in lambda calculus, Linear types and non-size-increasing polynomial time computation., Realizability models for BLL-like languages, Tiering as a Recursion Technique, The Computational SLR: A Logic for Reasoning about Computational Indistinguishability

Cites Work

• A new recursion-theoretic characterization of the polytime functions
• Logical relations and the typed λ-calculus
• An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
• Extensional Constructs in Intensional Type Theory
• Semantics of linear/modal lambda calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item