| layout | title | subtitle |
|---|---|---|
page |
Publications |
Papers about Proof General |
- David Aspinall and Christoph Lüth Beyond Script Management. Talk given at CIAO 2007. Slides in pdf (420k).
- David Aspinall. Eclipse Proof General. An Eclipse version of Proof General. Brief outline of plan available as pdf (128k).
- David Aspinall. Protocols for Interactive e-Proof. Unpublished draft. Available on request.
- David Aspinall. Proof General Kit (white paper). Unpublished draft. Available on request.
- See also the Proof General Kit web page.
- David Aspinall, Christoph Lüth and Daniel Winterstein. A Framework for Interactive Proof. Appears in Towards Mechanized Mathematical Assistants, Springer LNAI 4573, pp.161--175, 2007. Download as pdf (315k).
- David Aspinall, Christoph Lüth and Burkhart Wolff. Assisted Proof Document Authoring. Appears in Mathematical Knowledge Management 2005 (MKM '05), Springer LNAI 3863, p. 65--80, 2005. Download as pdf (307k).
- David Aspinall and Christoph Lüth. Proof General meets IsaWin --- combining text-based and graphical user interfaces. Long version of paper presented at UITP '03. Appears in ENTCS, Download as pdf (344k).
- Daniel Winterstein, David Aspinall, and Christoph Lüth. Proof General Eclipse: A Generic Interface for Interactive Proof. Draft paper. Download as pdf (389k).
- David Aspinall. Proof General: A Generic Tool for Proof Development. In Tools and Algorithms for the Construction and Analysis of Systems, Proc TACAS 2000, LNCS 1785. Download as ps.gz. Here are some slides used for this talk and some other presentations of Proof General.
- Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. In Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998. Download as ps.gz. This paper describes Script Management, also supported by Proof General.
- Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'Inria Sophia Antipolis: RR-3286. This paper describes PG's implementation of Proof by Pointing.