Lab for Foundations of Computer Science
School of Informatics
University of Edinburgh
4pm Tuesday 28 September 2004
Level 2, Appleton Tower
Names, binding, and alpha-equivalence are central concepts in many areas of computer science, especially in the study of programming langauges and logics. Until recently, there were only two real choices for programming and formal verification of systems involving names and binding: a direct approach in which names are implemented as strings and alpha-equivalence, renaming, substitution etc. are implemented manually, or the "higher-order abstract syntax" approach in which the variables and binding features provided by a powerful meta-language such as the lambda-calculus are used for names and binding in object-languages.
The first approach is the most practical but can be difficult to reason about because of the need to reason explicitly about substitution and renaming. The second approach can be easier to reason about in some respects but is semantically very complicated, so for example inductive proof principles are elusive.
Recently Gabbay and Pitts developed a third promising approach that seems to avoid many of the disadvantages of both prior approaches while preserving their advantages. In their approach, binding and substitution are formalized in terms of bijective renaming operations (or swappings). Pitts presented a variant of first-order logic called nominal logic that incorporates these ideas.
I (in collaboration with Christian Urban, University of Cambridge) have been developing an approach to logic programming based on nominal logic. I have developed a variant of Prolog called alphaProlog that incorporates these ideas. In this talk I will provide an overview of nominal logic and then describe the unification and resolution algorithms currently used in alphaProlog and show how they permit more convenient (and more transparently correct) logic programming with names and binding.