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

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...

Full description

Saved in:
Bibliographic Details
:
Breitner, Joachim
Year of Publication:2016
Language:English
Physical Description:1 electronic resource (XIV, 231 p. p.)
Tags: Add Tag
No Tags, Be the first to tag this record!
id 993548706504498
ctrlnum (CKB)4920000000094639
(oapen)https://directory.doabooks.org/handle/20.500.12854/51469
(EXLCZ)994920000000094639
collection bib_alma
fullrecord <?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>01481nam-a2200289z--4500</leader><controlfield tag="001">993548706504498</controlfield><controlfield tag="005">20231214133637.0</controlfield><controlfield tag="006">m o d </controlfield><controlfield tag="007">cr|mn|---annan</controlfield><controlfield tag="008">202102s2016 xx |||||o ||| 0|eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">1000056002</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(CKB)4920000000094639</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(oapen)https://directory.doabooks.org/handle/20.500.12854/51469</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(EXLCZ)994920000000094639</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Breitner, Joachim</subfield><subfield code="4">auth</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Lazy Evaluation: From natural semantics to a machine-checked compiler transformation</subfield></datafield><datafield tag="246" ind1=" " ind2=" "><subfield code="a">Lazy Evaluation</subfield></datafield><datafield tag="260" ind1=" " ind2=" "><subfield code="b">KIT Scientific Publishing</subfield><subfield code="c">2016</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 electronic resource (XIV, 231 p. p.)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">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.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">English</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle</subfield></datafield><datafield tag="776" ind1=" " ind2=" "><subfield code="z">3-7315-0546-0</subfield></datafield><datafield tag="906" ind1=" " ind2=" "><subfield code="a">BOOK</subfield></datafield><datafield tag="ADM" ind1=" " ind2=" "><subfield code="b">2023-12-15 06:01:04 Europe/Vienna</subfield><subfield code="f">system</subfield><subfield code="c">marc21</subfield><subfield code="a">2019-11-10 04:18:40 Europe/Vienna</subfield><subfield code="g">false</subfield></datafield><datafield tag="AVE" ind1=" " ind2=" "><subfield code="i">DOAB Directory of Open Access Books</subfield><subfield code="P">DOAB Directory of Open Access Books</subfield><subfield code="x">https://eu02.alma.exlibrisgroup.com/view/uresolver/43ACC_OEAW/openurl?u.ignore_date_coverage=true&amp;portfolio_pid=5338854440004498&amp;Force_direct=true</subfield><subfield code="Z">5338854440004498</subfield><subfield code="b">Available</subfield><subfield code="8">5338854440004498</subfield></datafield></record></collection>
record_format marc
spelling Breitner, Joachim auth
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
Lazy Evaluation
KIT Scientific Publishing 2016
1 electronic resource (XIV, 231 p. p.)
text txt rdacontent
computer c rdamedia
online resource cr rdacarrier
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.
English
Funktionale Programmierung Formale Verifikation Semantik Isabelle HaskellFunctional Programming Semantics Formal Verification Haskell Isabelle
3-7315-0546-0
language English
format eBook
author Breitner, Joachim
spellingShingle Breitner, Joachim
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
author_facet Breitner, Joachim
author_variant j b jb
author_sort Breitner, Joachim
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_auth Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
title_alt Lazy Evaluation
title_new Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
title_sort lazy evaluation: from natural semantics to a machine-checked compiler transformation
publisher KIT Scientific Publishing
publishDate 2016
physical 1 electronic resource (XIV, 231 p. p.)
isbn 1000056002
3-7315-0546-0
illustrated Not Illustrated
work_keys_str_mv AT breitnerjoachim lazyevaluationfromnaturalsemanticstoamachinecheckedcompilertransformation
AT breitnerjoachim lazyevaluation
status_str n
ids_txt_mv (CKB)4920000000094639
(oapen)https://directory.doabooks.org/handle/20.500.12854/51469
(EXLCZ)994920000000094639
carrierType_str_mv cr
is_hierarchy_title Lazy Evaluation: From natural semantics to a machine-checked compiler transformation
_version_ 1796649042756763649

Similar Items