Paper: Linear higher-order pre-unification (at LICS 1997)
Authors: Iliano. Cervesato Frank PfenningAbstract
We develop an efficient representation and a pre-unification algorithm in the style of Huet (1975) for the linear /spl lambda/-calculus /spl lambda//sup /spl rarr//spl rArr/0&T/ which includes intuitionistic functions (/spl rarr/), linear functions (/spl rArr/), additive pairing (&), and additive unit (T). Applications lie in proof scorch, logic programming, and logical frameworks based on linear type theories. We also show that, surprisingly, a similar pre-unification algorithm does not exist for certain sublanguages.
BibTeX
@InProceedings{CervesatoPfenning-Linearhigherorderpr, author = {Iliano. Cervesato and Frank Pfenning}, title = {Linear higher-order pre-unification}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {422--433}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }