Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twelfth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {422--433},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski