Stream Fusion for Isabelle's Code Generator
Rough Diamond
dc.contributor.author
Lochbihler, Andreas
dc.contributor.author
Maximova, Alexandra
dc.contributor.editor
Urban, Christian
dc.contributor.editor
Zhang, Xingyuan
dc.date.accessioned
2024-09-13T08:39:30Z
dc.date.available
2017-06-11T20:24:26Z
dc.date.available
2024-09-13T08:39:30Z
dc.date.issued
2015
dc.identifier.isbn
978-3-319-22101-4
en_US
dc.identifier.isbn
978-3-319-22102-1
en_US
dc.identifier.issn
0302-9743
dc.identifier.issn
1611-3349
dc.identifier.other
10.1007/978-3-319-22102-1_18
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/106019
dc.description.abstract
Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.
en_US
dc.language.iso
en
en_US
dc.publisher
Springer
en_US
dc.title
Stream Fusion for Isabelle's Code Generator
en_US
dc.type
Conference Paper
dc.date.published
2015-01-01
ethz.title.subtitle
Rough Diamond
en_US
ethz.book.title
Interactive Theorem Proving
en_US
ethz.journal.title
Lecture Notes in Computer Science
ethz.journal.volume
9236
en_US
ethz.journal.abbreviated
LNCS
ethz.pages.start
270
en_US
ethz.pages.end
277
en_US
ethz.event
6th International Conference on Interactive Theorem Proving (ITP 2015)
en_US
ethz.event.location
Nanjing, China
en_US
ethz.event.date
August 24-27, 2015
en_US
ethz.identifier.scopus
ethz.publication.place
Cham
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit / Institute of Information Security::03634 - Basin, David / Basin, David
en_US
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02660 - Institut für Informationssicherheit / Institute of Information Security::03634 - Basin, David / Basin, David
ethz.date.deposited
2017-06-11T20:24:43Z
ethz.source
ECIT
ethz.identifier.importid
imp5936539e638f448338
ethz.ecitpid
pub:165967
ethz.eth
yes
en_US
ethz.availability
Metadata only
en_US
ethz.rosetta.installDate
2017-07-15T04:48:10Z
ethz.rosetta.lastUpdated
2025-02-14T13:51:49Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Stream%20Fusion%20for%20Isabelle's%20Code%20Generator&rft.jtitle=Lecture%20Notes%20in%20Computer%20Science&rft.date=2015&rft.volume=9236&rft.spage=270&rft.epage=277&rft.issn=0302-9743&1611-3349&rft.au=Lochbihler,%20Andreas&Maximova,%20Alexandra&rft.isbn=978-3-319-22101-4&978-3-319-22102-1&rft.genre=proceeding&rft_id=info:doi/10.1007/978-3-319-22102-1_18&rft.btitle=Interactive%20Theorem%20Proving
Dateien zu diesem Eintrag
| Dateien | Größe | Format | Im Viewer öffnen |
|---|---|---|---|
|
Zu diesem Eintrag gibt es keine Dateien. |
|||
Publikationstyp
-
Conference Paper [36916]