Quicksort via Bird's Tree Fusion Transformation

Tjark Weber and James Caldwell. Published online at the Formal Digital Libraries Project, May 2003.

Abstract

In this paper we present a Nuprl formalization and proof of Bird's fusion theorem for trees. We apply the theorem to a derivation of quicksort.

Download

• Postscript (281 kB)
• PDF (292 kB)

BibTeX

@misc{weber03quicksort,
  author       = {Tjark Weber and James Caldwell},
  title        = {Quicksort via {Bird}'s Tree Fusion Transformation},
  howpublished = {Published online at the Formal Digital Libraries Project},
  month        = may,
  year         = {2003}
}