Gordon Plotkin has kindly shared the 2017 Alonzo Church Award announcement with me. I am happy to post it here and hope that readers of this blog will be enticed to learn about this truly fundamental contribution to theoretical computer science.
The 2017 Alonzo Church Award for Outstanding Contributions to Logic and Computation
is given jointly to Samson Abramsky, Radha Jagadeesan, Pasquale Malacaria,
Martin Hyland, Luke Ong, and Hanno Nickau for providing a fully-abstract semantics for
higher-order computation through the introduction of game models, thereby fundamentally
revolutionising the field of programming language semantics, and for the applied impact
of these models. Their contributions appeared in three papers:
- S. Abramsky, R. Jagadeesan, and P. Malacaria. Full Abstraction for PCF. Information and
Computation, Vol. 163, No. 2, pp. 409-470, 2000.
- J.M.E. Hyland and C.-H.L. Ong. On Full Abstraction for PCF: I, II, and III. Information
and Computation, Vol. 163, No. 2, pp. 285-408, 2000.
- H. Nickau. Hereditarily sequential functionals. Proc. Symp. Logical Foundations of Computer Science: Logic at St. Petersburg (eds. A. Nerode and Yu.V. Matiyasevich), Lecture
Notes in Computer Science, Vol. 813, pp. 253-264. Springer-Verlag, 1994.
Description of the Contribution
These papers made two fundamental contributions to our understanding of programming
languages and logic. First, they provided signi ficant insight into the longstanding and
fundamental "full abstraction problem" for the paradigmatic higher-order language PCF
by giving a compositional semantic account of sequentiality, via an elegant
cartesian-closed category of games and strategies. In the mid-1970s Milner posed the
full-abstraction problem for PCF and Plotkin showed the difficulty of the problem, which
essentially lies in the fact that the standard Scott-Strachey model permits non-sequential
functions, although PCF itself is sequential.
The papers constructed models for PCF from games, leading to the first fully abstract
models of PCF whose construction made no reference to the syntax of PCF. The
elements of the models are strategies for certain kinds of interactive dialogues between
two players (or between system and environment). These dialogue games are required to
follow certain conventions concerning when questions are posed or answered; these
conventions reflect constraints on the information available to the players of the game.
The papers give new insight into the fundamental work in higher-type recursion theory of
such logicians as Kleene, Gandy, Normann, and Hyland.
Second, and perhaps more importantly, game semantics has provided a new framework for
the semantics of programming languages. Games can be used as a
flexible and modular modelling tool, as a wide variety of programming language features can be understood as
corresponding to different restrictions placed on allowed strategies. Thus there are fully
abstract games models for call-by-value and call-by name languages; for languages with
state, with control, with references, with exceptions, with nondeterminism, and with
probability; and for concurrent and mobile process languages. In this way, game
semantics has changed the landscape of programming language semantics by giving a
unified view of the denotational universes of many different languages. This is a
remarkable achievement that was not previously thought to be within reach.
Techniques developed in game semantics have found their way into a wide variety of
applications. For example, they have provided tools for the verification of a range of
computational systems, such as reactive systems of timed and hybrid automata,
higher-order and mobile processes, and model-checking higher-order programs. There has
also been significant influence on other areas, for example, static program analysis, type
systems, resource-sensitive compilation, and compiler certification. All of these
developments can be traced from the initial work of Abramsky, Jagadeesan and
Malacaria, of Hyland and Ong, and of Nickau.
The 2017 award will be presented at the 26th Computer Science Logic (CSL) Conference,
the annual meeting of the European Association for Computer Science Logic. This will
be held August 20th{24th, 2017, at Stockholm University, Sweden.
The Alonzo Church Award for Outstanding Contributions to Logic and Computation was
established in 2015 by the ACM Special Interest Group for Logic and Computation
(SIGLOG), the European Association for Theoretical Computer Science (EATCS), the
European Association for Computer Science Logic (EACSL), and the Kurt Godel Society
(KGS). The award is for an outstanding contribution represented by a paper, or small
group of papers, within the past 25 years; this is the second such award. The 2017 Award
Committee consisted of Catuscia Palamidessi, Gordon Plotkin (chair), Natarajan
Shankar, and Moshe Vardi.
