Paul Levy - Call-By-Push-Value: A Subsuming Paradigm

Call-by-push-value (CBPV) is a new paradigm (based on work of Moggi and Filinski) that subsumes the call-by-name and call-by-value paradigms, in the following sense: both operational and denotational semantics for those paradigms can be seen as arising, via translations that we will provide, from similar semantics for CBPV. (Thus CBPV has applications to game semantics, continuation semantics and functor category semantics.) To explain CBPV, we first discuss general operational ideas, especially the distinction between values and computations, following the principle that ``a value is, a computation does''. Using an example program, we see that the lambda-calculus primitives can be understood as push/pop commands for an operand-stack. We provide operational and denotational semantics for a range of computational effects and show their agreement. We hence obtain semantics for call-by-name and call-by-value, of which some are familiar, some are new and some were known but previously appeared mysterious.