UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Analysing Resource Use in the Lambda Calculus by Type Inference

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. Green open access

[img]
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.

Type: Proceedings paper
Title: Analysing Resource Use in the Lambda Calculus by Type Inference
Event: ACM SIGPlan Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'94)
Location: Orlando, Florida, USA
Dates: 25 June 1994
Open access status: An open access version is available from UCL Discovery
Publisher version: https://compilers.iecc.com/comparch/article/94-04-...
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
UCL classification: UCL
UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10087132
Downloads since deposit
7Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item