@InBook{cutcontinuations,
  chapter = {Cutting Out Continuations},
  pages = {187--200},
  title = {A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday},
  publisher = {Springer International Publishing},
  year = {2016},
  author = {Graham Hutton and Patrick Bahr},
  editor = {Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don},
  month = mar,
  abstract = {In the field of program transformation, one often transforms
programs into continuation-passing style to make their flow of
control explicit, and then immediately removes the resulting
continuations using defunctionalisation to make the programs
first-order.  In this article, we show how these two transformations
can be fused together into a single transformation step that
cuts out the need to first introduce and then eliminate continuations.
Our approach is calculational, uses standard equational
reasoning techniques, and is widely applicable.},
  date = {2016-03-25},
  note = {Wadler Festschrift},
  doi = {10.1007/978-3-319-30936-1_10},
  isbn = {978-3-319-30936-1},
  keywords = {program calculation, verification, abstract machine, Rocq, equational reasoning},
  url = {http://dx.doi.org/10.1007/978-3-319-30936-1_10}
}