Call-by-push-value: Decomposing call-by-value and call-by-name

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 operaroperties: 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 ...

• Type: Journal
• Year: 2006
• Where: LISP
• Authors: Paul Blain Levy
• Keywords: CBPV, LISP 2006, Semantics, Typed Call-by-value