[TYPES/announce] HOSC paper on call-by-push-value

[Paul B Levy]

Dear colleagues, 

I'd like to announce a paper, just published in Higher-Order and Symbolic
Computation, about call-by-push-value, a canonical calculus for
computational effects that unifies call-by-value and call-by-name.  The
paper answers (I hope) all your questions about the similarities and
differences between call-by-push-value and the monad framework, but any
more questions or comments are very welcome!

regards,
Paul

----------------------------------------------

Call-by-push-value: decomposing call-by-value and call-by-name
Paul Blain Levy
Higher-Order and Symbolic Computation, vol. 19(4), December 2006.

Abstract

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 operational properties: 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 essentially the
same type structure as CBPV.  We also discuss less formally the
differences between the CBPV and monadic frameworks.

 
--
Paul Blain Levy              email: pbl at cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl