Ideas for the future of Proof General

Proof General Kit and PGIP

An Overview of Emacs Proof General

  • 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.