Accession Number:

ADA324652

Title:

A Linear Spine Calculus,

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1997-04-10

Pagination or Media Count:

36.0

Abstract:

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.

Subject Categories:

  • Operations Research
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE