Specification of analysis and transformation.

In [40], strictness analysis is formulated in terms of type inference. A type reconstruction algorithm is presented, and the strictness information is used to avoid some superfluous “thunkifications” when translating from call-by-name into call-by-value. Of particular interest is the proof technique: the correctness of the translation is proved simultaneously with the correctness of the analysis. The part concerning type reconstruction is published in [26]; the part concerning translation is published in [27].