Linear higher-order pre-unification

被引：5
|
作者：
Cervesato, I
Pfenning, F
机构：
来源：
12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 1997年
关键词：
D O I：
10.1109/LICS.1997.614967
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We develop an efficient representation and a pre-unification algorithm in the style of Huet for the linear lambda-calculus lambda(-->-O&T) which includes intuitionistic functions (-->), linear functions (-o), additive pairing (&), and additive unit (T). Applications lie in proof search, 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.
引用
收藏
页码：422 / 433
页数：12
相关论文
共 50 条
12345