Paper: Unification and anti-unification in the calculus of constructions (at LICS 1991)
Authors: Frank PfenningAbstract
Algorithms for unification and anti-unification in the calculus of constructions, where occurrences of free variables (the variables subject to instantiation) are restricted to higher-order patterns, are presented. Most general unifiers and least common anti-instances are shown to exist and are unique up to a simple equivalence. The unification algorithm is used for logic program execution and type and term reconstruction in the current implementation of Elf and has shown itself to be practical
BibTeX
@InProceedings{Pfenning-Unificationandantiu, author = {Frank Pfenning}, title = {Unification and anti-unification in the calculus of constructions }, booktitle = {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991}, year = 1991, editor = {Giles Kahn}, month = {July}, pages = {74--85}, location = {Amsterdam, The Netherlands}, publisher = {IEEE Computer Society Press} }