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.

Dieses Buch richtet sich an Lehrende an Hochschulen, Schulen und anderen Ausbildungseinrichtungen, an Hochschuldidaktiker mit Bezug zur Programmierausbildung und an Informatiker, die mit der Entwicklung oder Integration von Systemen zur automatischen Programmbewertung beschäftigt sind. Die Ziele dieses Buches sind zum einen, Lehrenden die praktische Relevanz und Tauglichkeit automatisierter Programmbewertung aufzuzeigen und damit deren Einsatz durch die Darstellung erfolgreicher Ansätze zu fördern. Zum anderen sollen dem Thema der automatisierten Programmbewertung ein größerer Bekanntheitsgrad in der Fachöffentlichkeit verschafft und Arbeitsergebnisse aus Forschungs- und Praxisprojekten einem größeren Anwenderkreis präsentiert werden.