DocumentCode
3300592
Title
Linear higher-order pre-unification
Author
Cervesato, Iliano ; Pfenning, Frank
Author_Institution
Dept. of Comput. Sci., Carnegie Mellon Univ., Pittsburgh, PA, USA
fYear
1997
fDate
29 Jun-2 Jul 1997
Firstpage
422
Lastpage
433
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
Conference_Location
Warsaw
ISSN
1043-6871
Print_ISBN
0-8186-7925-5
Type
conf
DOI
10.1109/LICS.1997.614967
Filename
614967
Link To Document