View the project on GitHub
Welcome to the Lemma Overloading project website! This project is part of coq-community.
This project contains Hoare Type Theory libraries which demonstrate a series of design patterns for programming with canonical structures that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and illustrates these patterns through several realistic examples drawn from Hoare Type Theory. The project also contains typeclass-based re-implementations for comparison.
This is an open source project, licensed under the GNU General Public License v3.0 or later.
The current stable release of Lemma Overloading can be downloaded from GitHub.
The coqdoc presentations of releases can be browsed online:
Other related publications, if any, are listed below.