language: en

A Linear Spine Calculus

Iliano Cervesato and Frank Pfenning 1
April 10, 1997 CMU-CS-97-125
School of Computer Science Carnegie Mellon University
Pittsburgh, PA 15213

Abstract We present the spine calculus S !ffi&&gt; as an efficient representation for the linear -calculus !ffi&&gt; which includes intuitionistic functions (!), linear functions (ffi), additive pairing (&), and additive unit (&gt;). S !ffi&&gt; enhances the representation of Church's simply typed -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 -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 !ffi&&gt; into S !ffi&&gt; 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.

[1 The authors can be reached at]

iliano@cs.cmu.edu and fp@cs.cmu.edu.