Research on "Formal Methods in Computing"

An Inference Algorithm for Strictness

ABSTRACT. In this paper we introduce an algorithm for detecting strictness information in typed functional programs. Our algorithm is based on a type inference system which allows to exploit the type structure of the language for the investigation of program properties. The detection of strictness information can be performed in a complete way, by reducing it to the solution of a set of constraints involving type variables. A key feature of our method is that it is compositional and there is a notion of principal type scheme. Even though the language considered in the paper is the simply typed lambda-calculus with a fixpoint constructor and arithmetic constants we can generalize our approach to polymorphic languages like Lazy ML. Although focused on strictness our method can also be applied to the investigation of other program properties, like dead code and binding time.

ps.gz ( © Springer-Verlag )

BIBTEX.

@conference{Damiani-Giannini:TLCA-97,
   author    = {F. Damiani and P. Giannini},
   title     = {{An Inference Algorithm for Strictness}},
   booktitle = {{TLCA'97}},
   year      = {1997},
   publisher = {Springer},
   pages     = {129-146},
   series    = {LNCS 1210}
}