[TYPES] new book

[Paul B Levy]

Dear type theorists,

My book "Call-By-Push-Value" has been published by Kluwer in the "Semantic 
Structures in Computation" bookseries

http://www.wkap.nl/prod/b/1-4020-1730-8

- 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:

"Call-By-Push-Value
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!

Regards
Paul
http://www.cs.bham.ac.uk/~pbl