The 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to Murdoch J. Gabbay and Andrew M. Pitts for their ground-breaking work introducing the theory of nominal representations.
The ACM Special Interest Group on Logic (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS) are pleased to announce that Murdoch J. Gabbay (Heriot-Watt University, UK) and Andrew M. Pitts (Cambridge University, UK) have been selected as the winners of the 2019 Alonzo Church Award for Outstanding Contributions to Logic and Computation. The award recognizes their ground-breaking work introducing the theory of nominal representations, a powerful and elegant mathematical model for computing with data involving atomic names, described in the following papers:
Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding, Formal Aspects of Computing 13(3):341– 363, 2002.
Andrew M. Pitts. Nominal logic, a first order theory of names and binding, Information and Computation 186(2):165–193, 2003.
Nominal techniques have had a major impact on a number of areas of computing and logic as a powerful framework for reasoning about formal languages for programming and modelling. The 2019 Church Award was selected by a panel consisting of Thomas Eiter, Javier Esparza, Radha Jagadeesan, Catuscia Palamidessi, and Natarajan Shankar.
The Contribution
These two papers represent an early, cornerstone contribution to a large body of work that has established nominal techniques as a general and highly influential approach to answering a key question in the semantics of programming languages: when is a mathematical structure used in the semantics of programming languages dependent upon, or independent from, some names? Those papers proposed to use nominal sets (introduced in set theory by Fraenkel and Mostowski in the 1930s) to provide a mathematical theory and an accompanying logic for some of the key concepts that arise when representing and computing with data involving atomic names, such as freshness, abstraction and scoping of names, and finiteness modulo symmetry. Over the last fifteen years, nominal techniques have become a fundamental tool for modelling locality in computation, underlying research presented in over a hundred papers, new programming languages and models of computation. They have applications to the syntax and semantics of programming languages, to logics for machine-assisted reasoning about programming-language semantics and to the automatic verification of specifications in process calculi. Variations on nominal sets are used in automata theory over infinite alphabets, with applications to querying XML and databases, and also feature in work on models of Homotopy Type Theory. This is a remarkable achievement for any formalism. It is even more remarkable that this achievement was accompanied by an elegant theory based on classic work in set theory, whose computer-science application has highlighted the importance of invariance under symmetry in modelling names and their scope.