A Linear Spine Calculus,
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
We present the spine calculus Sapproaches -oT as an efficient representation for the linear lambda-calculus lambdaapproaches -oT which includes intuitionistic functions approach Tau linear functions -oTau additive pairing Tau and additive unit T. Sapproaches -oT enhances the representation of Churchs simply typed lamda-calculus as abstract Bolum 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 searchTau logic programmingTau and logical frameworks based on linear type theories. We define the spine calculusTau give translations of lambdaapproaches -oT into Sapproaches -oT and vice-versaTau prove their soundness and completeness with respect to typing and reductionTau and shows that the spine calculus is strongly normalizing and admits unique canonical forms.
- Operations Research
- Computer Programming and Software