Courtenage, S; Clack, CD; (1994) Analysing Resource Use in the Lambda Calculus by Type Inference. In: Proceedings of the PEPM'94. (pp. pp. 33-41). University of Melbourne, Australia: Orlando, FL, USA.

Preview

Text AIL2.pdf - Accepted Version Download (180kB) | Preview

Abstract

If we view functions as processes, then their resources are their arguments, supplied through application, and used by the function to produce a result. In this paper, we define resource use for functions, based on the syntactic notion of needed redexes from [BKKS86]. We introduce a variant of neededhess, tail-neededness, and define packets of needed descendants of redexes in order to measure the degree of neededhess. These results are generalised to produce a semantic characterisation of the resource use properties of functions, using a term-model. By means of the Curry-Howard isomorphism, we apply these ideas to proof trees of propositions in Intuitionistic Logic to demonstrate that propositions, i.e. types, can be used to express the usage properties of functions. A resource-aware type system capable of inferring such types for L-terms is presented.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as XMLJSONCSV

Downloads by country - last 12 months

Export as XMLJSONCSV

Archive Staff Only

View Item