The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/21/2014 03:02 PM, Jonathan wrote:
> To all,
>
> If you're interested in a way to get full erasability in Coq, or yet 
> another encoding of Red/Black trees in Coq, have a look at:
>
> https://github.com/jonleivent/mindless-coding
>
> Erasability is accomplished by adding a single injectivity axiom to a 
> single wrapper Prop type (Erasable).

I haven't looked at your code, but the erasure approach sounds like what 
we did in Ynot (which is defunct at the moment).
Project web site: http://ynot.cs.harvard.edu/
Paper: http://adam.chlipala.net/papers/YnotICFP09/