Interactive Proof Presentations with Cobra

Martin Ring
Christoph Lüth
(DFKI and Universität Bremen)

We present Cobra, a modern proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows for live changes both by the presenter and the audience.

In Serge Autexier and Pedro Quaresma: Proceedings of the 12th Workshop on User Interfaces for Theorem Provers (UITP 2016), Coimbra, Portugal, 2nd July 2016, Electronic Proceedings in Theoretical Computer Science 239, pp. 43–52.
Published: 24th January 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: