N. Sculthorpe and G. Hutton, “Work it, wrap it, fix it, fold it,” Journal of Functional Programming, vol. 24, no. 1, pp. 113–127, 2014.

Links

• http://dx.doi.org/10.1017/S0956796814000045

• http://www.ittc.ku.edu/csdl/fpg/files/Sculthorpe-14-WorkIt.pdf

Abstract

The worker/wrapper transformation is a general-purpose technique for refactoring recursive programs to improve their performance. The two previous approaches to formalising the technique were based upon different recursion operators and different correctness conditions. In this article we show how these two approaches can be generalised in a uniform manner by combining their correctness conditions, how the theory can be extended with new conditions that are necessary (in addition to sufficient) to ensure the correctness of the worker/wrapper technique, and explore the benefits that result. All the proofs have been mechanically verified using the Agda system.

BibTeX

@article{Sculthorpe:14:WorkIt,
  author = {Neil Sculthorpe and Graham Hutton},
  title = {Work It, Wrap It, Fix It, Fold It},
  journal = {Journal of Functional Programming},
  pages = {113--127},
  volume = {24},
  number = {1},
  publisher = {Cambridge University Press},
  year = {2014},
}