The 2019 Alonzo Church Award

The 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, for introducing the theory of nominal representations, a powerful and elegant mathematical model for computing with data involving atomic names.

Nomination for the papers

• “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.

Proposed citation For the invention of nominal techniques, providing a highly influential mathematical model for key concepts that arise when computing with data involving atomic names.

Succinct description of the contribution The nominated papers are two early, cornerstone contributions 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.

Detailed statement In our research work, we all dream about offering some contribution to our field of study that is based on some elegant theoretical work, that paves the way to a substantial amount of follow-up research in a wide variety of fields related to logic in computer science, that leads to new models of computation and novel programming languages, and that is embodied in software tools that are already finding applications in academia and that might, one day, also have impact on software design and verification in industry. To our mind, the nominated papers by Murdoch (Jamie) Gabbay and Andrew Pitts achieved all those items on our wish list and provide a blueprint for truly outstanding research.

We find it hard to imagine a contribution to the field of logic in computer science 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 numbers 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, among 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 developed by Mark Shinwell and Andrew Pitts, and the αProlog logic programming language 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 stemming 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 Denotations 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 semantics 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, Gabbay 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 abstraction 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 substitution 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 introduced 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 related 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 contributions, 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 induction/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 equivariance 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 Computer 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 important 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

e-max.it: your social media marketing partner
 
European Association for Theoretical Computer Science - Maintained and hosted by RU1 / CTI.