Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Stream Fusion


view this post on Zulip Email Gateway (Aug 19 2022 at 16:18):

From: Lawrence Paulson <lp15@cam.ac.uk>
Stream Fusion in HOL with Code Generation
Andreas Lochbihler

Stream Fusion is a system for removing intermediate list data structures from functional programs, in particular Haskell. This entry adapts stream fusion to Isabelle/HOL and its code generator. We define stream types for finite and possibly infinite lists and stream versions for most of the fusible list functions in the theories List and Coinductive_List, and prove them correct with respect to the conversion functions between lists and streams. The Stream Fusion transformation itself is implemented as a simproc in the preprocessor of the code generator.

http://afp.sourceforge.net/entries/Stream_Fusion_Code.shtml

Larry Paulson


Last updated: Mar 28 2024 at 08:18 UTC