[TYPES] stacks in call-by-push-value

[Paul B Levy]

Dear all,

My paper "Adjunction models for Call-By-Push-Value with stacks", to appear 
in Theory and Applications of Categories (the special edition for CTCS 
2002), is on my webpage

http://www.cs.bham.ac.uk/~pbl/papers/

The abstract is below.  

regards
Paul


Call-by-push-value is a "semantic machine code", providing a set of simple
primitives from which both the call-by-value and call-by-name paradigms
are built. We present its operational semantics as a stack machine,
suggesting a term judgement of stacks. We then see that CBPV,
incorporating these stack terms, has a simple categorical semantics based
on an adjunction between values and stacks.  There are no coherence
requirements.

We describe this semantics incrementally. First, we introduce locally
indexed categories and the opGrothendieck construction, and use these to
give the basic structure for interpreting the three judgements: values,
stacks and computations. Then we look at the universal property required
to interpret each type constructor. We define a model to be a strong
adjunction with countable coproducts, countable products and exponentials.

We see a wide range of instances of this structure: we give examples for 
divergence, storage, erratic choice, continuations, possible worlds and 
games (with or without a bracketing condition), in each case resolving the 
strong monad from the literature into a strong adjunction.  And we give 
ways of constructing models from other models.

Finally, we see that call-by-value and call-by-name are interpreted within 
the Kleisli and co-Kleisli parts, respectively, of a call-by-push-value 
adjunction.