## The 2019 Alonzo Church AwardThe 2019 Alonzo Church Award committee consisting of Thomas Eiter, Javier Esparza, Radha Jagadeesan, Catuscia Palamidessi, and Natarajan Shankar, have selected Murdoch J. Gabbay and Andrew M. Pitts for the 2019 Church Award,
• “A new approach to abstract syntax with variable binding” by Murdoch J. Gabbay and Andrew M. Pitts, Formal Aspects of Computing 13(3):341– 363, 2002; and • “Nominal logic, a first order theory of names and binding” by Andrew M. Pitts, Information and Computation 186(2):165–193, 2003.
We find it hard to imagine a contribution to the field of logic in computer sci- ence over the last twenty five years that combines elegant and deep theory with such widespread impact in the research community. To wit, according to Google Scholar1 (last accessed on 25 February 2019 at 18:03 GMT), the FAC paper that we nominate, which was published in 2002, has so far received 852 citations, whereas the paper in In- formation and Computation has been cited 547 times since 2003. However, these num- bers of citations paint only a very partial picture of the truly remarkable impact that, in about fifteen years, the work on nominal techniques has had in several areas related to logic in computer science. Follow-up research based on the work presented in the two nominated papers, and others by those authors, their collaborators and colleagues, has been presented in over a hundred papers, and has led to new programming languages, models of computation and whole research programmes. Further evidence of the im- pact of nominal techniques are the PPDP most influential paper 10-year award 2014 given to “Nominal Rewriting Systems” by Maribel Ferna ́ndez, Jamie Gabbay and Ian Mackie, and the CADE Skolem Award 2015 to Christian Urban and Christine Tasson’s 2005 paper on “Nominal techniques in Isabelle/HOL”. Moreover, Christian Urban and Stefan Berghofer’s nominal package for Isabelle/HOL has been used, amongst others, by Joachim Parrow and his group in the development of the theory of the ψ-calculi and in its applications. Prototypical programming languages that are based on the ideas underlying the nominal techniques include the Fresh O’Caml functional programming language de- veloped by Mark Shinwell and Andrew Pitts, and the αProlog logic programming lan- guage of James Cheney and Christian Urban. More recently, Bartek Klin and Michal Szynwelski have developed Nλ2, a core programming language that aims at direct ma- nipulation of orbit-finite nominal sets. This programming language has been used in a paper presented at POPL 20173 to implement an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alpha- bets and have many applications in the verification of hardware and software systems. Moreover, at POPL 2017 Eryk Kopczynski and Szymon Torunczyk presented another programming language offering nominal support, LOIS (Looping Over Infinite Sets). Nominal techniques have had a major role in the development of semantic models for programming languages with generative effects. Starting from two papers in 2004 that introduced nominal denotational models for languages with private names (by Laird at FOSSACS 2004, and by Abramsky, Ghica, Murawski, Ong and Stark at LICS 2004), the area developed to the extent to model and supply verification techniques and tools for a variety of languages, ranging from ML variants, to fragments of Java and C- level code. These findings have been published in venues such as POPL, LICS, ESOP and TACAS, including earning a Kleene best student paper award at LICS 2007. The innovation offered by nominal techniques is simple yet crucial in modelling code: they provide a notion of abstract data type, a mathematically robust “black box type, that can represent a variety of computational entities, such as references, objects, channels and polymorphic abstractions, along with their effects. A further indication of the perceived importance of the nominal techniques stem- ming from the nominated papers within the theoretical computer science community as a whole is provided by the publication of the following recent papers in the very selective Journal of the ACM: • Murdoch James Gabbay. Semantics Out of Context: Nominal Absolute Denota- tions for First-Order Logic and Computation. J. ACM 63(3): 25:1–25 (2016). • Steffen Lo ̈sch, Andrew M. Pitts. Denotational Semantics with Nominal Scott Domains. J. ACM 61(4): 27:1–27 (2014). • Andrew M. Pitts. Alpha-structural recursion and induction. J. ACM 53(3): 459– 506 (2006). Most importantly, apart from their original application area in the syntax and seman- tics of programming languages, since their introduction a little over ten years ago, nominal techniques have been used in logics for machine-assisted reasoning about programming language semantics and in the automatic verification of specifications in process calculi, such as variants on the π-calculus. Variations on nominal sets are used in automata theory over infinite alphabets, with applications to querying XML and databases, Kleene algebra and co-algebra, universal algebra and equational logic, and also feature in work on models of Homotopy Type Theory. The conceptual framework and many of the technical ideas underlying the plethora of work we mentioned above were presented for the first time in the two nominated papers. The paper published in FAC introduced the notion of nominal set in the study of the syntax of programming languages with binding constructs. In that study, Gab- bay and Pitts showed how the permutation model of set theory with atoms, introduced by Fraenkel and Mostowski in the 1930s, supports the crucial notions of name abstrac- tion and fresh name, and that nominal sets provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding opera- tions. The crucial conceptual message in that paper is that inductively defined nominal sets can provide a faithful first-order treatment of abstract syntax modulo renaming of bound variables. This allows one to extend the classic theory of algebraic data types to signatures involving binding operators, providing an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substi- tution and set of free variables) and a notion of proof by structural induction. These are path-breaking contributions addressing a problem that had been open at least since Burstall’s 1969 paper “Proving properties of programs by structural induction”, and proposing a solution that is both elegant and pleasingly close to informal practice in computer science. This should be contrasted with the higher-order abstract syntax proposed by Alonzo Church himself, which is elegant but where many of the desirable properties mentioned above, such as accounts of structural recursion and induction, are missing. We find it truly remarkable that nominal techniques, which were originally in- troduced in the FAC paper to give a first-order treatment of abstract syntax modulo renaming of bound variables, have found such a fruitful application in many areas re- lated to logic in computer science and have led to the development of a nominal theory of computation, which is blossoming into an important area of research in theoretical computer science. The 2003 paper by Andrew Pitts introduced Nominal Logic, a version of first- order many-sorted logic with equality containing primitives for renaming via name- swapping, for freshness of names, and for name-binding. The axioms of Nominal Logic express properties of these constructs that hold in the nominal-set model of syn- tax involving binding presented in the FAC paper. Apart from its technical contribu- tions, the Information and Computation paper on Nominal Logic makes two important general points that have guided subsequent work. • Name-swapping suffices to provide a foundation for a theory of structural in- duction/recursion for syntax modulo α-equivalence and has much better logical properties than more general forms of renaming. • In the practice of operational semantics, one should make explicit the equivari- ance property of assertions about syntax, namely that their validity is invariant under name-swapping. These observations look very natural in hindsight, but, as far as we know, were not advocated before that paper. Gabbay and Pitts have also worked tirelessly to introduce nominal techniques within the theoretical-computer-science community. They did not limit themselves to writing technical papers on this fascinating topic, but they have also provided accounts of the theory in tutorials, surveys, graduate schools, workshops and books. Here we limit ourselves to mentioning the book “Nominal Sets: Names and Symmetry in Com- puter Science by Andrew Pitts (Cambridge University Press, May 2013), the lengthy survey paper “Foundations of nominal techniques: Logic and semantics of variables in abstract syntax by Murdoch Gabbay (Bulletin of Symbolic Logic 17(2):161–229, 2011) and the Dagstuhl Seminar 13422 on Nominal Computation Theory organized by Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz and Andrew Pitts in 2013. These outreach efforts have played an important role in making nominal techniques an im- portant and impactful topic in several areas in the theory of computation in a relatively short time span. For all the aforementioned reasons the main proposers of nominal techniques would be the perfect recipients of the 2019 Alonzo Church Award for Outstanding Contributions to Logic in Computation. We find it difficult to imagine a theoretical contribution to the field of the award that has had, and no doubt will continue to have, a comparable impact and that has stimulated so much follow-up research in such a wide variety of areas related to logic in computer science.
Luca Aceto, Gran Sasso Science Institute, L’Aquila, and Reykjavik University Marc Bezem, University of Bergen Mikolaj Bojanczyk, Warsaw University James Cheney, University of Edinburgh Thierry Coquand, Chalmers University of Technology Gilles Dowek, LSV, ENS Cachan, and ENS Paris-Saclay Peter Dybjer, Chalmers University of Technology Maribel Fernandez, King’s College London Bartek Klin, Warsaw University Dexter Kozen, Cornell University Alexander Kurz, University of Leicester Ugo Montanari, University of Pisa Andrzej Murawski, University of Warwick Luke Ong, University of Oxford Alexandra Silva, University College London Nikos Tzevelekos, Queen Mary University of London Stephanie Weirich, University of Pennsylvania |