A partial solution in Coq to the POPLmark Challenge using nested datatypes.
This is my on going effort to build the Zariski site in Coq. You can download the sources or browse the library online.
Up to now, it contains a library of category theory with basic constructions like the category of all cathegories, Yonda's emedding, Grothendieck topologies and some algebraic constructions.
AbGroup is a package I wrote for Coq to work with abelian group. It provides definitions and basic lemmas and a tactic "AbGroup" which help to normalize terms and to prove equations.
The tactic AbGroup uses a principle called "reflection". More complex examples are the analogous tactics for rings and fields already availlable in the standard Coq distribution.
There is no documentation yet, sorry. To learn how to use the tactic, start with the file abgroup_test.v in the distribution.
You can browse the sources online or download the package.
I also wrote a "coq mode" to run Coq as inferior Emacs process (screenshot):
It should work just fine under Gnu Emacs 21.