Sound and complete axiomatisations of call-by-value control operators

DOI10.1017/S0960129500001195zbMATH0846.68066OpenAlexW2034257290MaRDI QIDQ4882487FDOQ4882487

Authors Martin Hofmann

Publication date 15 July 1996

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129500001195

zbMATH Keywords

propositional logiccall-by-value \(\lambda\)-calculus

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Semantics in the theory of computing (68Q55)

Recommendations

• Axiomatizing subtyped delimited continuations
• A sound and complete axiomatization of delimited continuations
• scientific article; zbMATH DE number 7340561
• On the call-by-value CPS transform and its semantics
• Complete call-by-value calculi of control operators. II: Strong termination

Cites work

• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 46995 (Why is no real title available?)
• A syntactic theory of sequential control
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Notions of computation and monads

Cited in

(19)

• Decomposing typed lambda calculus into a couple of categorical programming languages
• A Semantical and Operational Account of Call-by-Value Solvability
• Axiomatizing subtyped delimited continuations
• On the semantics of classical disjunction
• scientific article; zbMATH DE number 2182491 (Why is no real title available?)
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• scientific article; zbMATH DE number 177801 (Why is no real title available?)
• Continuation-passing style models complete for intuitionistic logic
• Combining algebraic effects with continuations
• Complete call-by-value calculi of control operators. II: Strong termination
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• A type-theoretic foundation of delimited continuations
• scientific article; zbMATH DE number 1701354 (Why is no real title available?)
• A proof-theoretic foundation of abortive continuations
• Axioms for recursion in call-by-value
• A formal equational theory for call-by-push-value
• Domain-free \(\lambda\mu\)-calculus
• On the call-by-value CPS transform and its semantics
• Continuation calculus

This page was built for publication: Sound and complete axiomatisations of call-by-value control operators

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