Submitted by Jonathan Goddard on Wed, 17/04/2019 - 15:12
The ACM/IEEE Symposium on Logic in Computer Science (LICS) annual Test-of-Time Award recognises a small number of papers from the LICS proceedings from 20 years prior.
Two awards have been made in 2019 to honour outstanding papers from the IEEE Symposium on Logic in Computer Science 1999 held in Trento, Italy.
- A New Approach to Abstract Syntax Involving Binders by Murdoch Gabbay and Andrew M. Pitts
- Abstract Syntax and Variable Binding by Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi
Variable binding operators are pervasive in the study of programming languages and logics. Following an idea of Church (1940), these can be reduced to a single binding operator whose syntactic properties have been understood for some time. These two seminal papers propose contrasting approaches to achieve a matching semantic understanding for abstract syntax with binding.
Gabbay and Pitts employ the permutation model of set theory with atoms due to Fraenkel and Mostowski to represent name abstraction and fresh name generation. This led to a wealth of research using so-called nominal techniques, both in theory and in practical implementations in theorem provers. An extended and revised version of their paper was published in Formal Aspects of Computing in 2002.
Fiore, Plotkin, and Turi instead take a categorical approach, devising binding algebras that are presheaves endowed with both an algebra structure and a substitution structure that are compatible with each other. Abstract syntax with binding is then an initial model. The compatibility of this idea with de Bruijn indices, already popular in formal developments before 1999, has led to many applications of their results in further theory and implementations.
The awards will be presented at the 2019 LICS Symposium in Vancouver, in June.
