coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ML4PG announcement

From: "jonathanheras" <jonathanheras AT computing.dundee.ac.uk>
To: <coq-club AT inria.fr>, <proofgeneral AT informatics.ed.ac.uk>, <ssreflect AT msr-inria.inria.fr>
Subject: [Coq-Club] ML4PG announcement
Date: Tue, 18 Dec 2012 14:49:58 -0000

Title: ML4PG announcement

Dear all,

We have extended Proof General interface with a new functionality that
allows one to statistically analyse various patterns arising in Coq/SSReflect
proofs. Finding common patterns in proofs may be used as a guidance in big proof
developments across different users, as well as for educational/training purposes.
We have successfully tested it on several examples and libraries,
and are now looking for more users!

The tool will not alter your normal ProofGeneral routines --
but you will notice ProofGeneral will feature an extra option for
Proof Statistics.

More information can be found here:

http://www.computing.dundee.ac.uk/staff/katya/ML4PG/

We will be happy to hear your feedback.

Best,
Jónathan Heras and Katya Komendantskaya

The University of Dundee is a Scottish Registered Charity, No. SC015096.

[Coq-Club] ML4PG announcement, jonathanheras, 12/18/2012