TYPE INFERENCE, ABSTRACT INTERPRETATION AND STRICTNESS ANALYSIS

Filter domains (Coppo et al., 1984) can be seen as abstract domains fo r the interpretation of (functional) type-free programming languages. What is remarkable is the fact that in filter domains the interpretati on of a term is given by the set of its types in the intersection type discipline with inclusion, thus reducing the computation of an abstra ct interpretation to typechecking. As a main example, an abstract filt er domain for strictness analysis of type-free functional languages is presented. The inclusion relation between types representing strictne ss properties has a complete recursive axiomatization. Type inference rules cannot be complete (strictness being a PI1(0) property), but a c omplete extension of the type inference system is presented.