A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion

DOI10.1007/BFB0028020MaRDI QIDQ4218937zbMATH OpenFDO

Authors Martin Hofmann

Publication date 15 November 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0028020

zbMATH Keywords

category-theoretic modelhigher-order generalizations of Bellantoni-Cook's function algebralinear function spaceS4 modalitysimply-typed lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45)

Recommendations

• The Safe Lambda Calculus
• The Safe Lambda Calculus
• A linearization of the Lambda-calculus and consequences
• A mixed -calculus
• Semantics of linear/modal lambda calculus
• scientific article; zbMATH DE number 1420785
• On an interpretation of safe recursion in light affine logic
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• A Terminating and Confluent Linear Lambda Calculus
• Parametric domain-theoretic models of polymorphic intuitionistic/linear lambda calculus

Cited in

(23)

• Safe operators: Brackets closed forever. Optimizing optimal -calculus implementations
• Polytime, combinatory logic and positive safe induction
• Higher type recursion, ramification and polynomial time
• Safe recursion with higher types and BCK-algebra
• On an interpretation of safe recursion in light affine logic
• Combining linear logic and size types for implicit complexity
• Structural recursion as a query language on lists and ordered trees
• Formal security proofs with minimal fuss: implicit computational complexity at work
• A higher-order characterization of probabilistic polynomial time
• Higher-order interpretations and program complexity
• The geometry of linear higher-order recursion
• On equivalences, metrics, and polynomial time
• The best of both worlds: linear functional programming without compromise
• Probabilistic termination by monadic affine sized typing
• The Computational SLR: A Logic for Reasoning about Computational Indistinguishability
• A Calculus for Game-Based Security Proofs
• Combining linear logic and size types for implicit complexity
• Implicit computation complexity in higher-order programming languages
• The Safe Lambda Calculus
• The Safe Lambda Calculus
• Cyclic implicit complexity
• Primitive recursive dependent type theory
• Cyclic implicit complexity

This page was built for publication: A mixed modal/linear lambda calculus with applications to Bellantoni-Cook safe recursion

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