Title :
Linear higher-order pre-unification
Author :
Cervesato, Iliano ; Pfenning, Frank
Author_Institution :
Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
fDate :
29 Jun-2 Jul 1997
Abstract :
We develop an efficient representation and a pre-unification algorithm in the style of Huet (1975) for the linear λ-calculus λ→⇒0&T which includes intuitionistic functions (→), linear functions (⇒), 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
Keywords :
formal logic; lambda calculus; logic programming; programming theory; type theory; additive pairing; additive unit; intuitionistic functions; linear functions; linear higher-order pre-unification; linear lambda calculus; linear type theories; logic programming; logical frameworks; proof scorch; representation; sublanguages; Computer science; Ear; Encoding; Equations; Linearity; Logic design; Logic programming; Mathematics; Proposals; Writing;
Conference_Titel :
Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
Conference_Location :
Warsaw
Print_ISBN :
0-8186-7925-5
DOI :
10.1109/LICS.1997.614967
