Higher Order Demand Propagation as proposed in [Pa98] provides a non-standard denotational semantics for a realistic functional language. This semantics can be used to deduce generalised strictness information for higher order polymorphic functions. This report provides the formal proof for the correctness of this strictness information with respect to the non-strict standard semantics.
