Ordinal Notation and Computer Proof

Last ordinal post here

There is an implementation in Coq of the countable ordinals up to Γ₀.

More Proof of Referential Transparency

Previously, I talked about proving referential transparency. The authors of A Persistent Union-Find Data Structure (other version) use Coq to prove imperative functions referentially transparent, and they point out the work of Harold Baker, who designed fast persistent arrays (and here), which they also prove to be referentially transparent. These arrays are even available in Haskell, though wrapped in the IO monad.

The authors of the union-find paper say that their structure is not "purely applicative". I don't actually know what that means, but I suppose it means it's not strictly functional, since it requires in-place modification.

In any case, there are now at least four cases for being able to prove referential transparency so we can use it without wrapping everything in the IO monad:

• Memoization - For memoization in (not just for) Haskell, see this paper by the Simons and Conal Elliott. (mirror 1, mirror 2)
• Diff Arrays
• Splay Trees
• Union-Find

Any other ideas?