In order to solve a long-standing problem with list fusion a new compiler transformation Call
Arity is developed and implemented in the Haskell compiler GHC. It is formally proven to not
degrade program performance the proof is machine-checked using the interactive theorem prover
Isabelle. To that end a formalization of Launchbury's Natural Semantics for Lazy Evaluation is
modelled in Isabelle including a correctness and adequacy proof.
