Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
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 t...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Médium: | Online |
| Jazyk: | angličtina |
| Vydáno: |
KIT Scientific Publishing
2021
|
| Témata: | |
| On-line přístup: | 34320 |
| Tagy: |
Žádné tagy, Buďte první, kdo vytvoří štítek k tomuto záznamu!
|
| _version_ | 1869518255041806336 |
|---|---|
| author | Breitner, Joachim |
| author_browse | Breitner, Joachim |
| author_facet | Breitner, Joachim |
| author_sort | Breitner, Joachim |
| collection | Directory of Open Access Books |
| description | 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. |
| format | Online |
| id | doab-20.500.12854ir-51469 |
| institution | Directory of Open Access Books |
| language | eng |
| publishDate | 2021 |
| publishDateRange | 2021 |
| publishDateSort | 2021 |
| publisher | KIT Scientific Publishing |
| publisherStr | KIT Scientific Publishing |
| record_format | ojs |
| spelling | doab-20.500.12854ir-514692023-12-20T18:40:44Z Lazy Evaluation: From natural semantics to a machine-checked compiler transformation Breitner, Joachim QA75.5-76.95 Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle bic Book Industry Communication::U Computing & information technology::UY Computer science 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. 2021-02-11T17:29:50Z 2021-02-11T17:29:50Z 2019-07-30 20:01:57 2016 book 34320 9783731505464 https://directory.doabooks.org/handle/20.500.12854/51469 eng image/jpeg Attribution-ShareAlike 4.0 International https://www.ksp.kit.edu/9783731505464 KIT Scientific Publishing 10.5445/KSP/1000056002 10.5445/KSP/1000056002 68fffc18-8f7b-44fa-ac7e-0b7d7d979bd2 9783731505464 XIV, 231 p. open access |
| spellingShingle | QA75.5-76.95 Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle bic Book Industry Communication::U Computing & information technology::UY Computer science Breitner, Joachim Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title_full | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title_fullStr | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title_full_unstemmed | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title_short | Lazy Evaluation: From natural semantics to a machine-checked compiler transformation |
| title_sort | lazy evaluation from natural semantics to a machine checked compiler transformation |
| topic | QA75.5-76.95 Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle bic Book Industry Communication::U Computing & information technology::UY Computer science |
| topic_facet | QA75.5-76.95 Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle bic Book Industry Communication::U Computing & information technology::UY Computer science |
| url | 34320 |
| work_keys_str_mv | AT breitnerjoachim lazyevaluationfromnaturalsemanticstoamachinecheckedcompilertransformation |