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

@inproceedings{Voi08a, 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.}, address = {New York, NY, USA}, author = {Voigtl\"{a}nder, Janis}, booktitle = {PEPM '08: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation}, citeulike-article-id = {2297194}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1328408.1328412}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1328408.1328412}, citeulike-linkout-2 = {http://wwwtcs.inf.tu-dresden.de/~voigt/pepm09-voigtlaender.pdf}, doi = {10.1145/1328408.1328412}, editor = {Gl\"{u}ck, Robert and de Moor, Oege}, isbn = {9781595939777}, keywords = {deforestation, denotational-semantics, free-theorems, functional-programming, haskell, logical-relations, parametricity, polymorphism, program-transformation, rank-2, selective-strictness, seq, shortcut-deforestation, types}, month = {January}, pages = {13--20}, posted-at = {2008-01-28 10:20:36}, priority = {0}, publisher = {ACM Press}, title = {Proving Correctness via Free Theorems: The Case of the destroy/build-Rule}, url = {http://dx.doi.org/10.1145/1328408.1328412}, year = {2008} }

TY - CONF ID - Voi08a L3 - citeulike-article-id:2297194 N2 - 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. SN - 9781595939777 AD - New York, NY, USA EP - 20 TI - Proving Correctness via Free Theorems: The Case of the destroy/build-Rule PB - ACM Press T2 - PEPM '08: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation SP - 13 KW - deforestation KW - denotational-semantics KW - free-theorems KW - functional-programming KW - haskell KW - logical-relations KW - parametricity KW - polymorphism KW - program-transformation KW - rank-2 KW - selective-strictness KW - seq KW - shortcut-deforestation KW - types AU - Voigtländer, Janis A2 - Glück, Robert A2 - de Moor, Oege PY - 2008/01// UR - http://dx.doi.org/10.1145/1328408.1328412 ER -