Subject: categories: new book: Call-By-Push-Value

From: Paul B Levy <[email-masked]>
Date: Wed, 17 Mar 2004 12:37:05 +0000 (GMT)

Dear category 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 categorical structure of
the programming language - an adjunction between values and stacks - is
now completely apparent.

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