This book is a revised edition of the monograph which appeared under the
same title in the series Research Notes in Theoretical Computer Science,
Pit- man, in 1986. In addition to a general effort to improve
typography, English, and presentation, the main novelty of this second
edition is the integration of some new material. Part of it is mine
(mostly jointly with coauthors). Here is brief guide to these additions.
I have augmented the account of categorical combinatory logic with a
description of the confluence properties of rewriting systems of
categor- ical combinators (Hardin, Yokouchi), and of the newly developed
cal- culi of explicit substitutions (Abadi, Cardelli, Curien, Hardin,
Levy, and Rios), which are similar in spirit to the categorical
combinatory logic, but are closer to the syntax of A-calculus (Section
1.2). The study of the full abstraction problem for PCF and extensions
of it has been enriched with a new full abstraction result: the model of
sequential algorithms is fully abstract with respect to an extension of
PCF with a control operator (Cartwright, Felleisen, Curien). An order-
extensional model of error-sensitive sequential algorithms is also fully
abstract for a corresponding extension of PCF with a control operator
and errors (Sections 2.6 and 4.1). I suggest that sequential algorithms
lend themselves to a decomposition of the function spaces that leads to
models of linear logic (Lamarche, Curien), and that connects
sequentiality with games (Joyal, Blass, Abramsky) (Sections 2.1 and
2.6).