Relevant Logic and Strictness Analysis
Clem Baker-Finch. In Workshop on Static Analysis, LaBRI, Bordeaux, 1992. Bigre 81-82, pages 221-228.
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. The
result is a language of types containing strictness information, and a
corresponding type assignment system. Thus, information about the
reduction behaviour of a lambda-expression can be deduced at the same
time that its type is being inferred.
BibTeX, PostScript, gzipped PostScript