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)

Full work available at URL https://doi.org/10.1016/S0168-0072(00)00010-5

zbMATH Keywords

Bellantoni-Cook's function algebra

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• Logical relations and the typed λ-calculus
• Semantics of linear/modal lambda calculus

Cited in

(26)

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

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)