Stream Fusion for Isabelle’s Code Generator
Stream fusion is a popular optimisation technique initially proposed for Haskell by Duncan Coutts. In my bachelor thesis I formalized stream fusion for Isabelle/HOL's lists and embedded the transformation in Isabelle/HOL's code generator. The framework includes streamed versions of most standard list functions from the theory Main and is provided with a user interface to simplify the extension with own list functions. The code can be found in the theory Stream_Fusion_List that can be downloaded below.
For further information and instructions on how to extend the framework with own functions please consult the report. The framework was tested on artificial micro-benchmarks, execution time and allocated space of the generated code was measured. The test programs and the test results are available for download as a .zip file. For details on the test setup and evaluation I refer to the report.