[Club2] talk by Carst Tankink: Friday, August 23, 10:00, Room Turing (00.09.38)

[Andrei Popescu]

Dear All, 

Next Friday we have a talk by Carst Tankink on a problem that surely each of us 
has faced, perhaps painfully, at some point: documentation of formal proof developments. 
   
Cheers, 
   Andrei  

Documentation and Formal Mathematics: Web Technology meets Proof Assistants
Carst Tankink
Radboud University of Nijmegen
============================================================================
Friday, August 23, 10:00, Room Turing (00.09.38)

As the field of interactive theorem proving gains more high-impact projects
(both in mathematics and computer science), it becomes a necessity to document
and disseminate the artefacts of formal proof, in particular the proof scripts
used as input to the proof assistant.
In this talk, I will describe several workflows for describing and publishing
formal proofs, using modern web technologies. These workflows are implemented in
a single prototype 'Wiki' platform, that supports formalizations in the Coq and
HOL Light proof assistants, and I will use the system to demonstrate some of the
workflows.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130815/d008b079/attachment.html>