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].