Abstract
In this paper we propose an equational theory of a lambda calculus with names, name abstraction, and restriction, and a derived unification algorithm for this theory. Our calculus is very closely related to the calculus of Pitts 2011 [3]. We restrict the calculus presented there to obtain soundness of additional equalities, allowing us to define a unification algorithm very similar to the one given for the lambda calculus. We discuss the properties of this algorithm and give examples of its utility in meta-programming.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 25th International Workshop on Unification (UNIF 2011) |
| Pages | 42-51 |
| Number of pages | 10 |
| Publication status | Published - 2011 |