Logic in Computer Science (LICS 1997)

Paper: Linear higher-order pre-unification (at LICS 1997)

Authors: Iliano. Cervesato Frank Pfenning

Abstract

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}
  }