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.