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.

Call-by-push-value is a new programming language paradigm based on a slogan: A Value Is, A Computation Does. Levy (computer science, U. of Birmingham) presents evidence that it provides the semantic primitives from which the call-by-value and call-by-name paradigms are built, drawing from a wide range of semantics, including operational semantics in big-step and machine form; and denotational models using domains, possible worlds, continuations, and games. He looks at its equational theory from the perspectives of the call-by-value and call-by-name paradigms in the presence of general computational effects; at simple models for printing, divergence, global store, errors, erratic choice, and control effects; and at categorical semantics.
Annotation ©2004 Book News, Inc., Portland, OR (booknews.com)

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.

From the Contents: List of Figures. Preface. Acknowledgements. Introduction.- Part I: Language.- Part II: Concrete Semantics.- Part III: Categorical Semantics.- Part IV: Conclusions. Appendices.