Explore
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
Joachim Breitner
2016
0 Ungluers have
Faved this Work
Login to Fave
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.
This book is included in DOAB.
Why read this book? Have your say.
You must be logged in to comment.
Rights Information
Are you the author or publisher of this work? If so, you can claim it as yours by registering as an Unglue.it rights holder.Downloads
This work has been downloaded 15 times via unglue.it ebook links.
- 15 - pdf (CC BY-SA) at Unglue.it.
Keywords
- Computer science
- Computing & information technology
- Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle
Links
DOI: 10.5445/KSP/1000056002Editions