CMU-CS-97-125
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-97-125

A Linear Spine Calculus

Iliano Cervesato, Frank Pfenning

April 1997

CMU-CS-97-125.ps


Keywords: Linear lambda calculus, abstract Bohm trees, term assignment systems, uniform provability


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