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

DOI10.1017/S0960129500001195zbMATH Open0846.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

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

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)

Cites Work

• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Notions of computation and monads
• A syntactic theory of sequential control

Cited In (16)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Combining algebraic effects with continuations
• Continuation-passing style models complete for intuitionistic logic
• A Semantical and Operational Account of Call-by-Value Solvability
• A type-theoretic foundation of delimited continuations
• A proof-theoretic foundation of abortive continuations
• A formal equational theory for call-by-push-value
• Domain-free \(\lambda\mu\)-calculus
• Title not available (Why is that?)
• Axioms for recursion in call-by-value
• On the call-by-value CPS transform and its semantics
• On the semantics of classical disjunction
• Decomposing typed lambda calculus into a couple of categorical programming languages

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)