Call-by-Push-Value: ASubsuming Paradigm (Extended Abstract)
Paul Blain Levy · 1999
Call-by-push-value is a new paradigm 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 call-by-observable. To explain call-by-observable, we rst discuss general operational ideas, especially the distinction between values and computations, using the principle that \a value is, a computation does. Using an example pro- gram, 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 com- putational eects 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.