by Venanzio Capretta
The following files are an implementation in the proof system Coq (version 6.2.3) of the basic notions and results of Universal Algebra. The development is inspired by the presentation of Universal Algebra in the article by K. Meinke and J. V. Tucker in the Handbook of Logic in Computer Science.
Download the following archive file to get all the sources of the development: universal_algebra.tar.gz
A description of the work can be found in my paper Universal Algebra in Type Theory .
Any comment or suggestion is welcome. You can e-mail me at the address email@example.com.
Back to Home Page