Usage Analysis with Natural Reduction Types

Clem Baker-Finch & David Wright. In Third International Workshop on Static Analysis, Padova, 1993, LNCS vol. 724, pages 254-266.

Abstract

In a functional program the value of an expression may be required several times. If a usage analysis can determine how many times it will be required, certain optimisations are possible, such as converting lazy parameter passing to call-by-name or call-by-value, compile-time garbage collection and in-place update. This paper presents a method for deducing usage information in the lambda-calculus, based on a type logic employing reduction types. A system is presented wherein function type constructors are annotated with expressions over the natural numbers to indicate the usage behaviour of lambda-terms. This system is shown to be correct by interpreting the type language over a semi-model of the lambda-calculus and demostrating soundness and completeness. Furthermore, we show how the Curry-Howard interpretation naturally relates such types to relevant logic.

BibTeX, PostScript, gzipped PostScript