Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
| dc.contributor.author | Breitner, Joachim | * |
| dc.date.accessioned | 2021-02-11T17:29:50Z | |
| dc.date.available | 2021-02-11T17:29:50Z | |
| dc.date.issued | 2016 | * |
| dc.date.submitted | 2019-07-30 20:01:57 | * |
| dc.identifier | 34320 | * |
| dc.identifier.uri | https://directory.doabooks.org/handle/20.500.12854/51469 | |
| dc.description.abstract | 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. | * |
| dc.language | English | * |
| dc.subject | QA75.5-76.95 | * |
| dc.subject.classification | bic Book Industry Communication::U Computing & information technology::UY Computer science | en_US |
| dc.subject.other | Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle | * |
| dc.title | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation | * |
| dc.type | book | |
| oapen.identifier.doi | 10.5445/KSP/1000056002 | * |
| oapen.relation.isPublishedBy | 68fffc18-8f7b-44fa-ac7e-0b7d7d979bd2 | * |
| oapen.relation.isbn | 9783731505464 | * |
| oapen.pages | XIV, 231 p. | * |
| peerreview.review.type | Full text | |
| peerreview.anonymity | All identities known | |
| peerreview.reviewer.type | Internal editor | |
| peerreview.reviewer.type | External peer reviewer | |
| peerreview.review.stage | Pre-publication | |
| peerreview.open.review | No | |
| peerreview.publish.responsibility | Scientific or Editorial Board | |
| peerreview.id | 8ad5c235-9810-49eb-b358-27c8675324d9 | |
| peerreview.title | Dissertations (Dissertationen) |
Files in this item
| Files | Size | Format | View |
|---|---|---|---|
|
There are no files associated with this item. |
|||
This item appears in the following Collection(s)
Except where otherwise noted, this item's license is described
as
https://creativecommons.org/licenses/by-sa/4.0/