@InProceedings{Tullsen-Hudak:PEPM99,
  author =       "Mark Tullsen and Paul Hudak",
  title =        "Shifting expression procedures into reverse",
  year =         1999,
  booktitle =    "Proceedings of the {ACM} {SIGPLAN} Workshop on
                  Partial Evaluation and Semantics-Based Program Manipulation",
  editor =       "Olivier Danvy",
  series =       "Technical report BRICS-NS-99-1, University of Aarhus",
  address =      "San Antonio, Texas",
  month =        Jan,
  pages =        "95-104",
  abstract =     "The best known approach to program transformation is
                  the unfold/fold methodology of Burstall and
                  Darlington: a simple, intuitive, and expressive
                  approach which serves as the basis of many automatic
                  program transformation algorithms (such as partial
                  evaluation and deforestation).  Unfortunately
                  unfold/fold does not preserve total correctness and
                  requires maintaining a transformation history of the
                  program.  Scherlis invented a similar approach,
                  expression procedures, which solved these two
                  problems: expression procedures preserve total
                  correctness and require no transformation history.

                  Motivated by our desire to make expression
                  procedures more expressive by eliminating their
                  one-directional nature (they are designed to
                  specialize but not to generalize functions), we have
                  developed an equational specification of expression
                  procedures, in which the essence of expression
                  procedures is expressed in a single transformation
                  rule.  Our approach has the following advantages
                  over expression procedures: (1) all program
                  derivations are reversible; (2) transformations can
                  be done which expression procedures cannot do; (3)
                  fewer and simpler rules are used; and (4) the proof
                  of correctness is simpler.",
}