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 significant insight into the long-standing 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 non-determinism, 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.