We present the spine calculus S^{-> -o&T} as an efficient representation for the linear lambda-calculus lambda ^{-> -o&T} which includes intuitionistic functions (->), linear functions - ^o , additive pairing (&), and additive unit T. S^{-> -o&T} enhances the representation of Church's simply typed lambda-calculus as abstract Bohm trees by enforcing extensionality and by incorporating linear constructs. This approach permits procedures such as unification to retain the efficient head access that characterizes first-order term languages without the overhead of performing n-conversions at run time. Potential applications lie in proof search, logic programming, and logical frameworks based on linear type theories. We define the spine calculus, give translations of lambda ^{-> -o&T} into S ^{-> -o&T} and vice-versa, prove their soundness and completeness with respect to typing and reductions, and show that the spine calculus is strongly normalizing and admits unique canonical forms. 36 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu