I'm forwarding the message below because I think that this book could
interest this list.
It is the revised and simplified PhD thesis of Paul Blain Levy,
the culmination of his work on the subject. You can read the abstract
and an excerpt of a preceding paper here:
"Call-By-Push-Value: A Subsuming Paradigm"
----- Original Message -----
From: "Paul B Levy" <P.B.Levy at cs.bham.ac.uk>
Sent: Wednesday, March 17, 2004 1:43 PM
Subject: new book
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> Dear type theorists,
> My book "Call-By-Push-Value" has been published by Kluwer in the "Semantic
> Structures in Computation" bookseries
> - and I hope it will be of interest to many people on this list.
> Although it is based on my PhD thesis, subsequent research has led to a
> great deal of simplification. In particular, the introduction of a typing
> judgement (and denotational semantics) for stacks has made both the
> individual models and the categorical structure more straightforward and
> less mysterious.
> Here's the blurb:
> A Functional/Imperative Synthesis
> "Call-by-push-value is a programming language paradigm that, surprisingly,
> breaks down the call-by-value and call-by-name paradigms into simple
> primitives. This monograph, written for graduate students and researchers,
> exposes the call-by-push-value structure underlying a remarkable range of
> semantics, including operational semantics, domains, possible worlds,
> continuations and games.
> "After introducing basic ideas using domain semantics and a stack machine,
> the book is layered to appeal to readers in a variety of fields. One
> strand treats semantics of store, culminating in a possible world model
> for general storage cells. Another "implements" call-by-push-value by
> translating it into the Jump-With-Argument continuation language, enabling
> an account of pointer game semantics that explains its arenas, pointers
> and question/answer labelling in concrete computational terms. Yet another
> gives a categorical picture of call-by-push-value: an adjunction between
> values and stacks.
> "Incorporating recent simplifications, this is a key text for anyone
> interested in lambda-calculus, programming language foundations or
> applications of category theory."
> Please feel free to email me, either about the book or about the subject!