The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

All sorts of tree variants have invariants, although the RB tree
implementation is already quite a behemoth :-).

You can probably take anything in Okasaki's book [1] and try to do
that, I'd assume.  A lot of those datastructures have a style of a
"simple" and more complex implementation.  You could easily try to
prove the functional correctness of the complex implementation with
respect to the reference implementation, perhaps hidden behind a
module, if you wanted to get some practice with the module system.

As an example, I've always thought the functional queue reversal trick
was really cute.  You could definitely try that as an exercise
(http://www.cs.cornell.edu/courses/cs3110/2011sp/recitations/rec07.htm).

Kris


[1] Purely Functional Data Structures
     
http://www.amazon.com/Purely-Functional-Structures-Chris-Okasaki/dp/0521663504

On Mon, Apr 14, 2014 at 2:50 AM, Ömer Sinan Ağacan 
<omeragacan AT gmail.com>
 wrote:
> 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