Courtenage, Simon A.; (1996) The Analysis of Resource Use in the λ-Calculus by Type Inference. Doctoral thesis (Ph.D), UCL (University College London).

Text The_analysis_of_resource_use_i.pdf Download (3MB)

Abstract

This thesis is concerned primarily with the definition and semantics of resource use in the λ-calculus and the implicational fragment of intuitionistic propositional logic. A secondary aim is the subsequent derivation of a type system which can infer the expected reduction behaviour of functions upon their arguments. The term resource use refers to the view of arguments as the resources a function requires to produce a result. In this thesis, resource use will be taken to mean a property of the formal parameter of a function that describes the use that the function will make of arguments substituted for the parameter. Knowledge of the resource use of a function parameter can lead to many practical benefits in the efficient compilation of functional programs. Recent research has investigated the derivation of resource use information using type inference. Types inferred for functions contain resource use information about the way that arguments will be evaluated when applied to those functions. However, the justification of the correctness of these type systems relies on the given interpretation of type expressions as sets of terms possessing those types. The main contribution of this thesis is the definition of resource use in both the λ-calculus and in the implicational fragment of intuitionistic propositional logic that corresponds to the typed λ-calculus under the Curry-Howard isomorphism. We are able to demonstrate the correspondence of resource use between (typed) λ-terms and the proofs in intuitionsitic logic, though we find that this correspondence is not up to equivalence. Subsequently, we derive a type system for inferring resource use in λ-terms and also discuss the implementation of the type system. We find that we are unable to apply previously-used methods of unification over types containing resource use information when the range of resource use information is expanded.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as XMLCSVJSON

Archive Staff Only

View Item