| Unfolding Abstract Datatypes (2008) | |||||||||||||||
Abstract | |||||||||||||||
| Abstract. One of the most fundamental tools in the programmer’s toolbox is the abstract datatype. However, abstract datatypes are not as widely used in functional programming as they might be, 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 for reasoning with abstract datatypes. 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 the solution to a problem in the recent literature. 1 | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||