Part of
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.
Umfang: XIV, 231 S.
Preis: €36.00 | £33.00 | $63.00
These are words or phrases in the text that have been
automatically identified by the
Named Entity Recognition and Disambiguation service,
which provides Wikipedia
(
)
and Wikidata
(
)
links for these entities.
Breitner, J. 2016. Lazy Evaluation: From natural semantics to a machine-checked compiler transformation. Karlsruhe: KIT Scientific Publishing. DOI: https://doi.org/10.5445/KSP/1000056002
Dieses Buch ist lizenziert unter Creative Commons Attribution + ShareAlike 3.0 DE Dedication
Dieses Buch ist Peer reviewed. Informationen dazu finden Sie hier
Veröffentlicht am 20. September 2016
Englisch
256
| Paperback | 978-3-7315-0546-4 |