Relevance and Contraction: A Logical Basis for Strictness and Sharing Analysis

Clem Baker-Finch. University of Canberra Research Report, 1993, ISE RR 34/94.

Abstract

The concept of strictness in the simply-typed lambda-calculus is closely connected to implication in relevant logic. This connection is inspected and formalised via the Curry-Howard isomorphism. Various extensions are possible, resulting in a language of types containing strictness information, and a corresponding type assignment system. Thus, information about the strictness of a lambda-expression can be deduced at the same time that its type is being calculated. It is only a small step to also monitor applications of the contraction structural rule. This leads directly to use-count types containing unified strictness and sharing information. Soundness and completeness results demonstrate the correctness of this type system. The practicality of this approach, beyond the lambda-calculus paradigm, is addressed by the consideration of its application to some simple, typical functional programming language features.

BibTeX, PostScript, gzipped PostScript