Loading...
Please wait, while we are loading the content...
Similar Documents
Abstract Proving Correctness via Free Theorems
| Content Provider | CiteSeerX |
|---|---|
| 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. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Free Theorem Abstract Proving Correctness Correctness Issue Case Study Pure Functional Language Theoretical Foundation Potential Nontermination New Transformation Rule Destroy Build-rule Formal Method Semantic Aspect Intermediate List Program Transformation Foldr Build Certain Reconciliation Correctness Proof Mixed Strict Nonstrict Evaluation Semantic Property Short Cut Fusion Family |
| Content Type | Text |
| Resource Type | Article |
