Stream Fusion for Isabelle's Code Generator
Rough Diamond
METADATA ONLY
Loading...
Author / Producer
Date
2015
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Book title
Interactive Theorem Proving
Journal / series
Volume
9236
Pages / Article No.
270 - 277
Publisher
Springer
Event
6th International Conference on Interactive Theorem Proving (ITP 2015)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David