coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] First alpha release of Coq Modulo Theory

From: Pierre-Yves Strub <pierre-yves.strub AT inria.fr>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] First alpha release of Coq Modulo Theory
Date: Tue, 22 Jun 2010 15:58:41 +0800
Organization: INRIA

Dear Coq Club Mailing List,

I am pleased to announce the first release of CoqMT, an extension of
the Coq proof assistant (8.2) embedding, in its computational
mechanism, validity entailment for user-defined first-order equational
theories.

More details, along with source code, can be found on this web-page:

http://pierre-yves.strub.nu/research/coqmt/

Please, report comments and bugs to
pierre-yves AT strub.nu

Pierre-Yves Strub.

[Coq-Club] First alpha release of Coq Modulo Theory, Pierre-Yves Strub