Paper: Higher-order Unification via Explicit Substitutions (at LICS 1995)
Authors: Gilles Dowek Therese Hardin Claude KirchnerAbstract
Higher-order unification is equational unification for beta-eta- conversion. But it is not first-order equational unification, as substitution has to avoid capture. In this paper higher-order unification is reduced to first-order equational unification in a suitable theory: the lambda-sigma-calculus of explicit substitutions.
BibTeX
@InProceedings{DowekHardinKirchner-HigherorderUnificat, author = {Gilles Dowek and Therese Hardin and Claude Kirchner}, title = {Higher-order Unification via Explicit Substitutions}, booktitle = {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995}, year = 1995, editor = {Dexter Kozen}, month = {June}, pages = {366-374}, location = {San Diego, CA, USA}, publisher = {IEEE Computer Society Press} }