Contributions offered by Paul Blain Levy for topics 
D (verification methods)

Call-by-observable is a new paradigm (based on, but different from
Moggi's monad approach) 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 first discuss general operational
ideas, especially the distinction between values and
computations, using 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.

--------------------------------------------------------------
Result of feedback form submitted by
Levy (pbl@dcs.qmw.ac.uk) on Thursday, July 23, 1998 at 20:29:5