Strictness types: An inference algorithm and an application

This report deals with strictness types, a way of recording whether a function needs its argument(s) or not. We shall present an inference system for assigning strictness types to expressions and subsequently we transform this system into an algorithm capable of annotating expressions with strictness types. We give an example of a transfor-mation which can be optimized by means of these annotations, and finally we prove the correctness of the optimized transformation — at the same time proving the correctness of the annotation. Everything has been implemented; documentation can be found in appendix