Notes on “Unfolding Abstract Datatypes”

October 12, 2008

Unfolding Abstract Datatypes: Jeremy Gibbons

I read the first few pages, then skimmed the rest.

The Gist (I think): unfold is the key to making proofs about abstract datatypes. In the past, functional programmers have avoided abstract datatypes due to the difficulty of reasoning about them and the power of pattern matching. Gibbons gives a proof technique that eliminates the proof barrier.


(Why, Zachary, why?)

%d bloggers like this: