
Accession Number : ADA324652
Title : A Linear Spine Calculus,
Corporate Author : CARNEGIEMELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Cervesato, Iliano ; Pfenning, Frank
PDF Url : ADA324652
Report Date : 10 APR 1997
Pagination or Media Count : 36
Abstract : We present the spine calculus S(approaches o&T) as an efficient representation for the linear lambdacalculus lambda(approaches o&T) which includes intuitionistic functions (approach) Tau linear functions (o)Tau additive pairing (&Tau) and additive unit (T). S(approaches o&T) enhances the representation of Church's simply typed lamdacalculus 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 firstorder term languages without the overhead of performing nconversions at run time. Potential applications lie in proof search(Tau) logic programming(Tau) and logical frameworks based on linear type theories. We define the spine calculus(Tau) give translations of lambda(approaches o&T) into S(approaches o&T) and viceversa(Tau) prove their soundness and completeness with respect to typing and reduction(Tau) and shows that the spine calculus is strongly normalizing and admits unique canonical forms.
Descriptors : *LINEAR PROGRAMMING, *CALCULUS, *SYMBOLIC PROGRAMMING, ALGORITHMS, LINEAR SYSTEMS, COMPUTER LOGIC, PROGRAMMING LANGUAGES, SEMANTICS.
Subject Categories : Operations Research
Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE