KIT | KIT-Bibliothek | Impressum

Lazy Evaluation: From natural semantics to a machine-checked compiler transformation

Breitner, Joachim



Abstract (englisch): 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.


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Hochschulschrift
Jahr 2016
Sprache Englisch
Identifikator DOI: 10.5445/KSP/1000056002
ISBN: 978-3-7315-0546-4
URN: urn:nbn:de:0072-560028
KITopen ID: 1000056002
Verlag KIT Scientific Publishing, Karlsruhe
Umfang XIV, 231 S.
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Programmstrukturen und Datenorganisation (IPD)
Prüfungsdaten 25.04.2016
Referent/Betreuer Prof. G. Snelting
Schlagworte Funktionale Programmierung Formale Verifikation Semantik Isabelle Haskell Functional Programming Semantics Formal Verification Haskell Isabelle
Bestellung Die Veröffentlichung ist bei KIT Scientific Publishing erschienen.
Weitere Informationen sowie gegebenenfalls Bestellmöglichkeiten finden Sie hier.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page