Proof General meets IsaWin

We describe the design and prototype implementation of a combination of theorem prover interface technologies. On one side, we take from Proof General the idea of a prover-independent interaction language and its proposed implementation within the PG Kit middleware architecture. On the other side, we take from IsaWin a sophisticated graphical metaphor using direct manipulation for developing proofs. We believe that the resulting system will provide a powerful, robust and generic environment for developing proofs within interactive proof assistants that also opens the way for studying and implementing new mechanisms for managing interactive proof development.
David Aspinall and Christoph Lüth. Proof General meets IsaWin.
Proc. User Interfaces for Theorem Provers 2003 (UITP'03) September 2003, Rome, Italy. Extended version published in ENTCS, 103, 2004, pp3-26.
Download as pdf.

Click here to return to my papers page.

my Vcard
David R. Aspinall, email
Contact GPG key (Instant HOWTO)