[Prev][Next][Index][Thread]
thesis available
Dear colleagues,
My PhD thesis "Call-By-Push-Value" is available at
http://cs-people.bu.edu/pbl/papers/thesisqmwphd.ps.gz
The abstract is below.
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
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.