The Coq mailing list

[Carst Tankink <carst AT cs.ru.nl>]

Dear Coq-Club,

It is my pleasure to announce the first release of Proviola, a set of 
tools to create dynamic web pages out of Coq proof scripts and 
Coqdoc-generated HTML pages, allowing readers to inspect proof states 
without having to load the script into the proof assistant. We 
originally reported on its development during MKM and UITP, both in 2010 
[1,2]

You can read more about Proviola, and obtain the tool, at 
http://mws.cs.ru.nl/proviola/index.html

I will be happy to hear your thoughts about the tool!

Sincerely,
Carst Tankink

[1] Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk. 
Proviola: a tool for proof re-animation. Intelligent Computer 
Mathematics, volume LNAI 6167 of Lecture Notes in Artifical 
Intelligence, pages 440 - 454. March 2010. Preprint available through 
http://cs.ru.nl/~carst/files/proviola.pdf.
[2]    Carst Tankink, Herman Geuvers, and James McKinna. Narrating 
formal proof (work in progress). In User Interfaces for Theorem Provers 
2010. To appear in an issue of ENTCS. Available through 
http://www.cs.ru.nl/~carst/files/narration.pdf