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

Functional programming and lambda calculus (68N18) BCK-algebras, BCI-algebras (06F35) Semantics in the theory of computing (68Q55) Complexity of computation (including implicit computational complexity) (03D15) Higher-type and set recursion theory (03D65)

Related Items

Higher-order interpretations and program complexity ⋮ A new “feasible” arithmetic ⋮ Light affine lambda calculus and polynomial time strong normalization ⋮ On Equivalences, Metrics, and Polynomial Time ⋮ Linear types and non-size-increasing polynomial time computation. ⋮ The calculus of dependent lambda eliminations ⋮ Build your own clarithmetic I: Setup and completeness ⋮ Realizability models and implicit complexity ⋮ Type inference for light affine logic via constraints on words ⋮ A Calculus for Game-Based Security Proofs ⋮ A semantic proof of polytime soundness of light affine logic ⋮ The computational SLR: a logic for reasoning about computational indistinguishability ⋮ Light types for polynomial time computation in lambda calculus ⋮ Tiering as a Recursion Technique ⋮ A Formalization of Polytime Functions ⋮ The Computational SLR: A Logic for Reasoning about Computational Indistinguishability ⋮ Realizability models for BLL-like languages ⋮ Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Aspects of Categorical Recursion Theory ⋮ Quantitative classical realizability ⋮ Formal security proofs with minimal fuss: implicit computational complexity at work ⋮ Implicit computation complexity in higher-order programming languages

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