Recently Gabbay and Pitts developed a promising approach that seems to avoid many of the disadvantages of prior approaches to abstract syntax with names and binding 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) 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 programming and show how it permits more convenient (and more transparently correct) logic programming with names and binding.

One significant problem with nominal logic programming is that the unification and backchaining problems that must be solved are both NP-complete and algorithmically complex (that is, showing membership in NP is not trivial). In this talk I will present two recent contributions: techniques for identifying clauses for which alphaProlog's naive proof search algorithm works properly, and algorithms for solving the NP-complete unification problems effectively (if not efficiently).