Safe recursion with higher types and BCK-algebra

DOI10.1016/S0168-0072(00)00010-5MaRDI QIDQ1577481zbMATH OpenFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 1223626
• Higher type recursion, ramification and polynomial time
• Semantics of linear/modal lambda calculus
• scientific article; zbMATH DE number 1531370

Cites work

• scientific article; zbMATH DE number 445159 (Why is no real title available?)
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 1223626 (Why is no real title available?)
• scientific article; zbMATH DE number 1231474 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 2079048 (Why is no real title available?)
• scientific article; zbMATH DE number 1390027 (Why is no real title available?)
• scientific article; zbMATH DE number 3305097 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• A new recursion-theoretic characterization of the polytime functions
• An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
• Extensional Constructs in Intensional Type Theory
• Logical relations and the typed λ-calculus
• Semantics of linear/modal lambda calculus

Cited in

(25)

• The computational SLR: a logic for reasoning about computational indistinguishability
• Light types for polynomial time computation in lambda calculus
• A Calculus for Game-Based Security Proofs
• A new “feasible” arithmetic
• Higher-order interpretations and program complexity
• Realizability models and implicit complexity
• Implicit computation complexity in higher-order programming languages
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• Realizability models for BLL-like languages
• Quantitative classical realizability
• Light affine lambda calculus and polynomial time strong normalization
• Formal security proofs with minimal fuss: implicit computational complexity at work
• Build your own clarithmetic. I: Setup and completeness
• Linear types and non-size-increasing polynomial time computation.
• On equivalences, metrics, and polynomial time
• A formalization of polytime functions
• On an interpretation of safe recursion in light affine logic
• Type inference for light affine logic via constraints on words
• Aspects of categorical recursion theory
• The calculus of dependent lambda eliminations
• Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs
• Tiering as a Recursion Technique
• Safe operators: Brackets closed forever. Optimizing optimal \(\lambda\)-calculus implementations
• A semantic proof of polytime soundness of light affine logic
• Proof-theoretic semantics and feasibility

This page was built for publication: Safe recursion with higher types and BCK-algebra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1577481)