@inproceedings{Gibbons2008:Unfolding,
  abstract = "One of the most fundamental tools in the programmer's toolbox is the abstract datatype. However, abstract datatypes are not widely used in functional programming, perhaps because they are not subject to familiar proof methods such as equational reasoning and induction — in essence, because they are a form of codata rather than a form of data. We show that proof methods for corecursive programs are the appropriate techniques to use. In particular, building on established work on final coalgebra semantics for object-oriented programs, we show that the reasoning principles of unfold operators are perfectly suited for the task. We illustrate with solutions to two recent problems in the literature.",
  author = "Jeremy Gibbons",
  booktitle = "Mathematics of Program Construction",
  month = "jul",
  title = "Unfolding Abstract Datatypes",
  url = "http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/adt.pdf",
  year = "2008",
}