Call-By-Push-Value: A Subsuming Paradigm

[Massimo Dentico]

Paul Blain Levy, "Call-By-Push-Value: A Subsuming Paradigm"

- http://www.disi.unige.it/conferences/appsem98/proceedings/levy.ps.gz
- http://citeseer.nj.nec.com/357549.html

==================================================================
Abstract.  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-push-value.
To   explain   call-by-push-value,  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.

[...]

10 Practical Issues

CBPV  has emerged as a common theoretical foundation for  CBN  and
CBV.  We  speculate that, with the addition of suitable  syntactic
sugar,  it  could  provide  a basis for  a  practical  programming
language. Firstly, the operand-stack interpretation of lambda  and
application  illustrated  in  Sect. 2.3  seems  fairly  intuitive.
Secondly,  the  separation  of  the  two  parts  of  CBV   lambda-
abstraction (viz. thunk and lambda) makes currying of functions  -
problematic in CBV (cf. [16]) — as easy as in CBN, because of  the
isomorphism
                              ~
                (A x A’) -> B = A -> (A’ -> B)
                            ¯               ¯

    Furthermore (CBPV gives rise to more equivalences than  either
CBN  or  CBV  which could benefit implementers. Specifically,  the
comparatively simple continuation semantics of Sect. 6 might allow
efficient compilation along the lines of [3].

[...]
==================================================================

Proceedings of APPSEM'98 (ESPRIT WG APPlied SEMantics)

- http://www.disi.unige.it/conferences/appsem98/proceedings/

Esprit Working Group 26142 - Applied Semantics

- http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/


-- 
Massimo Dentico