CoqParam is the starting point of an implementation of a generator of "theorems for free" in Coq, based on parametricity theory. For the moment, it is made up with a tactic and a vernacular command that, given a closed Coq term and its type, compute: It is a new way to prove some theorems in Coq, like commutation theorems.

This is a prototype, and lots of things remain to do! In particular, it would be nice to be able to automatically instantiate the free theorems with the right parametricity relations to automatically solve Coq goals.

It is mainly developed by Chantal Keller at École Polytechnique and INRIA Saclay-Île-de-France and Marc Lasson at École Normale Supérieure de Lyon.


The source code is distributed under the terms of the GNU Lesser General Public License, version 3.
Download: To compile it, please report to the installation instructions available in the archive.

Top of the page


The code of the tactic comes with different examples, situated in the Examples directory:

Top of the page

Suggestions and bugs report

Do not hesitate to make any suggestion or to report bugs to Chantal Keller (remove the anti-spam dots and at).

Top of the page

Last update: 04/08/12