The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

I'm learning dependently typed programming in Coq and I'd like know
some good algorithms/data structures for exercising certified
programming. These algorithms/data structures are probably need to
have some invariants that can be encoded in type system or some
theorems that an user would like to know it's proved.

Does anyone here know some examples of this kind of algorithms/data
structures? I'm looking for something other than the ones in CPDT and
SF.

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net