- Cartan's Theorem in HOL Light
- Formalization of Lambda Calculus in Coq and HOL
- A solution for the POPLmark challenge
- The Zariski site in Coq
- JMeq implies eq
- AbGroup : A Coq tactic for abelian groups
- Coq mode

## Cartan's Theorem in HOL Light

A Formalization of Cartan's theorem in HOL.
(Very draft, see files and README.txt
and cartan.pdf for a brief
introduction.)
## Formalization of Lambda Calculus in Coq and HOL

A formal developement in two theorem prover (Coq
and HOL-Light) of the syntax and semantics of pure (untyped) Lambda
Calculus by means of the natural notion of moudules over a monad.
## A solution for the POPLmark challenge

A partial solution in Coq to the POPLmark
Challenge using nested datatypes.

## The Zariski site in Coq

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.

## JMeq implies eq

A proof that, under *Proof Irrelevance*, `JMeq` implies
`eq`. Download the file `jmeq.v`
for Coq V8.
## AbGroup : A Coq tactic for abelian groups

**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.

## Coq mode

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.