
- Breitner, Joachim
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
- Dissertationsschrift
- Kartoniert,
- KIT Scientific Publishing
- (2016)
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.
In order to solve a long-standing problem ...
DETAILS
- Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
- Dissertationsschrift
- Breitner, Joachim
- Kartoniert, 256 S.
- graph. Darst.
- Sprache: Englisch
- 21 cm
- ISBN-13: 978-3-7315-0546-4
- Titelnr.: 59910681
- Gewicht: 350 g
- KIT Scientific Publishing (2016)
Herstelleradresse
KIT Scientific Publishing
Strasse am Forum 2
76131 - DE Karlsruhe
E-Mail: info@ksp.kit.edu