Proving Correctness via Free Theorems: The Case of the destroy/build-Rule

The paper is available via the ACM DL Author-ize feature:

ACM DL Author-ize service Proving Correctness via Free Theorems: The Case of the destroy/build-Rule

Author: J. Voigtländer
Published: In Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'08, acceptance rate 20/74), San Francisco, California, Proceedings, pages 13-20, ACM, January 2008.
DOI: 10.1145/1328408.1328412
BibTeX: Voi08a.bib
Abstract: Free theorems feature prominently in the field of program transformation for pure functional languages such as Haskell. However, somewhat disappointingly, the semantic properties of so based transformations are often established only very superficially. This paper is intended as a case study showing how to use the existing theoretical foundations and formal methods for improving the situation. To that end, we investigate the correctness issue for a new transformation rule in the short cut fusion family. This destroy/build-rule provides a certain reconciliation between the competing foldr/build- and destroy/unfoldr-approaches to eliminating intermediate lists. Our emphasis is on systematically and rigorously developing the rule's correctness proof, even while paying attention to semantic aspects like potential nontermination and mixed strict/nonstrict evaluation.
Download: http://dl.acm.org/authorize?936382 (free)
Slides: Slides of my talk at the conference are here.

The tool used in this paper to derive free theorems is now accessible via a web interface here. (The paper itself mentions an older link.)