Subject: categories: Call-By-Push-Value thesis available

From: Paul Levy <[email-masked]>
Date: Tue, 26 Jun 2001 13:03:01 -0400 (EDT)

Dear colleagues,

My PhD thesis "Call-By-Push-Value" is available at

http://cs-people.bu.edu/pbl/papers/thesisqmwphd.ps.gz

The call-by-push-value paradigm is based to a large extent on the
theory of adjunctions.  Part 3 of the thesis explains this
connection, so I hope it will be of especial interest to category theorists. 

Regards
Paul Blain Levy, Boston University
http://cs-people.bu.edu/pbl/

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

Call-By-Push-Value
PhD thesis, Queen Mary, University of London, March 2001

Abstract

Call-by-push-value (CBPV) is a new programming language paradigm,
based on the slogan ``a value is, a computation does''.  We claim that
CBPV provides the semantic primitives from which the call-by-value and
call-by-name paradigms are built.   The primary goal of the thesis is
to present the evidence for this claim, which is found in a remarkably
wide range of semantics: from operational semantics, in big-step form
and in machine form, to denotational models using domains, possible
worlds, continuations and games. 

In the first part of the thesis, we come to CBPV and its equational
theory by looking critically at the call-by-value and call-by-name
paradigms in the presence of general computational effects.  We give a
Felleisen/Friedman-style CK-machine semantics, which explains how CBPV
can be understood in terms of push/pop instructions. 

In the second part we give simple CBPV models for printing,
divergence, global store, errors, erratic choice and control effects,
as well as for various combinations of these effects.  We develop the
store model into a possible world model for cell generation, and
(following Steele) we develop the control model into a ``jumping
implementation'' using a continuation language called
Jump-With-Argument (JWA). 

We present a pointer game model for CBPV, in the style of Hyland and
Ong. We see that the game concepts of questioning and answering
correspond to the CBPV concepts of forcing and producing respectively.
We observe that this game semantics  is closely related to the jumping
implementation.

In the third part of the thesis, we study the categorical semantics
for the CBPV equational theory.  We present and compare 3 approaches: 
\begin{itemize}
\item models using \emph{strong monads}, in the style of Moggi;
\item models using \emph{value/producer structures}, in the style of Power
  and Robinson;
\item models using (strong) adjunctions.
\end{itemize}
All the concrete models in the thesis are seen to be adjunction models.