Sound and complete axiomatisations of call-by-value control operators
Martin O. Hofmann · Mathematical Structures in Computer Science · 1995
We formulate a typed version of call-by-value λ-calculus containing variants of Felleisen's control operators A and C that provide explicit access to continuations and logically extend the propositions-as-types correspondence to classical propositional logic. We give an equational theory for this calculus, which is shown to be sound and complete with respect to a class of categorical models based on continuation-passing-style semantics.