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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Coutts, D.: Stream fusion: practical shortcut fusion for coinductive sequence types. Ph.D. thesis, University of Oxford (2010)
Coutts, D., Leshchinskiy, R., Stewart, D.: Stream fusion: from lists to streams to nothing at all. In: ICFP 2007, pp. 315–326. ACM (2007)
Farmer, A., Höner zu Siederdissen, C., Gill, A.: The HERMIT in the stream. In: PEPM 2014, pp. 97–108. ACM (2014)
Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: FPCA 1993, pp. 223–232. ACM (1993)
Haftmann, F., Krauss, A., Kunčar, O., Nipkow, T.: Data refinement in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 100–115. Springer, Heidelberg (2013)
Huffman, B.: Stream fusion. Archive of Formal Proofs, formal proof development (2009). http://afp.sf.net/entries/Stream-Fusion.shtml
Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167–183. Springer, Heidelberg (2014)
Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84–99. Springer, Heidelberg (2013)
Lochbihler, A.: Light-weight containers for Isabelle: efficient, extensible, nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 116–132. Springer, Heidelberg (2013)
Lochbihler, A., Hölzl, J.: Recursive functions on lazy lists via domains and topologies. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 341–357. Springer, Heidelberg (2014)
Lochbihler, A., Maximova, A.: Stream fusion in HOL with code generation. Archive of Formal Proofs, formal proof development (2014). http://afp.sf.net/entries/Stream_Fusion_Code.shtml
Sternagel, C., Thiemann, R.: Ceta 2.18. http://cl-informatik.uibk.ac.at/software/ceta/ (2014)
Svenningsson, J.: Shortcut fusion for accumulating parameters & zip-like functions. In: ICFP 2002, pp. 124–132. ACM (2002)
Acknowledgements
We thank Joachim Breitner for helping with analysing the GHC compilation. He, Ralf Sasse, and David Basin helped to improve the presentation.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Lochbihler, A., Maximova, A. (2015). Stream Fusion for Isabelle’s Code Generator. In: Urban, C., Zhang, X. (eds) Interactive Theorem Proving. ITP 2015. Lecture Notes in Computer Science(), vol 9236. Springer, Cham. https://doi.org/10.1007/978-3-319-22102-1_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-22102-1_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22101-4
Online ISBN: 978-3-319-22102-1
eBook Packages: Computer ScienceComputer Science (R0)