Safe recursion with higher types and BCK-algebra

DOI10.1016/S0168-0072(00)00010-5zbMATH Open0959.68075MaRDI QIDQ1577481FDOQ1577481

Authors: Martin Hofmann 

Publication date: 4 September 2000

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A new recursion-theoretic characterization of the polytime functions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Logical relations and the typed λ-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Extensional Constructs in Intensional Type Theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Semantics of linear/modal lambda calculus
• An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras

Cited In (25)

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

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)