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.
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