Higher-Order Unification for the λαν calculus

James Cheney, Ben Kavanagh

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish
Title of host publicationProceedings of the 25th International Workshop on Unification (UNIF 2011)
Number of pages10
Publication statusPublished - 2011

Cite this