
CMUCS97125
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS97125
A Linear Spine Calculus
Iliano Cervesato, Frank Pfenning
April 1997
CMUCS97125.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 lambdacalculus
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 lambdacalculus 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
firstorder term languages without the overhead of performing
nconversions 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 viceversa, 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
