Skip to main content

Unfolding Abstract Datatypes

Jeremy Gibbons

Abstract

Abstract datatypes — with public interfaces hiding private implementations — represent a form of codata rather than ordinary data, and so proof methods for corecursive programs are the appropriate techniques to use for reasoning with them. In particular, we show that the universal properties of unfold operators are perfectly suited for the task. We illustrate with the solution to a problem in the recent literature.

Book Title
Mathematics of Program Construction
Month
jul
Year
2008