Interesting. The extensions to the type system remind me of Ωmega (http://code.google.com/p/omega/ http://code.google.com/p/omega/), though without higher-order

Interesting. The extensions to the type system remind me of Ωmega (http://code.google.com/p/omega/ http://code.google.com/p/omega/), though without higher-order kinds. EDIT: Turns out "Programming in Omega" is cited by the section on related work. No wonder the mention of proving red-black trees using type-level computation seemed familiar...