Email Gateway (Aug 18 2022 at 13:28): Email Gateway (Aug 18 2022 at 13:28):From: Tobias Nipkow <nipkow@in.tum.de>
Stream Fusion
Brian Huffman
Stream Fusion is a system for removing intermediate list structures from
Haskell programs; it consists of a Haskell library along with several
compiler rewrite rules. (The library is available online at
http://www.cse.unsw.edu.au/~dons/streams.html.
These theories contain a formalization of much of the Stream Fusion
library in HOLCF. Lazy list and stream types are defined, along with
coercions between the two types, as well as an equivalence relation for
streams that generate the same list. List and stream versions of map,
filter, foldr, enumFromTo, append, zipWith, and concatMap are defined,
and the stream versions are shown to respect stream equivalence.
Enjoy!
Tobias
PS This is the first AFP entry to build on HOLCF, HOL's extension with
domain theory!
Last updated: May 03 2024 at 08:18 UTC