| Abstract: | We present the call-by-push-value (CBPV) calculus, which decomposes the typed call-by-value (CBV) and typed call-by-name (CBN)
paradigms into fine-grain primitives. On the operational side, we give big-step semantics and a stack machine for CBPV, which
leads to a straightforward push/pop reading of CBPV programs. On the denotational side, we model CBPV using cpos and, more
generally, using algebras for a strong monad. For storage, we present an O’Hearn-style “behaviour semantics’’ that does not
use a monad.
We present the translations from CBN and CBV to CBPV. All these translations straightforwardly preserve denotational semantics.
We also study their operational properties: simulation and full abstraction.
We give an equational theory for CBPV, and show it equivalent to a categorical semantics using monads and algebras. We use
this theory to formally compare CBPV to Filinski’s variant of the monadic metalanguage, as well as to Marz’s language SFPL,
both of which have essentially the same type structure as CBPV. We also discuss less formally the differences between the
CBPV and monadic frameworks. |
