Marco Maggesi - Mechanized Mathematics

1. Cartan's Theorem in HOL Light
2. Formalization of Lambda Calculus in Coq and HOL
3. A solution for the POPLmark challenge
4. The Zariski site in Coq
5. JMeq implies eq
6. AbGroup : A Coq tactic for abelian groups
7. Coq mode

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):

• coq.el - an Emacs mode to edit Coq vernacular files. Born as a modification of the Coq mode written by Jean-Christophe Filliâtre.
• inferior-coq.el - an Emacs mode to run an inferior Coq process.

It should work just fine under Gnu Emacs 21.