Proof General - A General Tool for Proof Development

This paper describes how proof texts are constructed and edited in the Proof General Kit framework. The framework includes user-oriented display components, connected to provers via a central broker component. The display components and the broker exchange messages in a format specified by the PGIP display protocol.

David Aspinall, Christoph Lüth and Daniel Winterstein.
Parsing, Editing, Proving: The PGIP Display Protocol.
Presented at International Workshop on User Interfaces for Theorem Provers 2005 (UITP'05).
Download as pdf.

Click here to return to my papers page.

David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)