Proof General Kit

Proof General Kit is our implementation of the PGIP protocol and interface architecture. It consists of:

• A Haskell middleware component, the ProofGeneralBroker
• Front end components, including
  • ProofGeneralEclipse
  • NewProofGeneralEmacs
  • PGWin

All of these components are under development and not yet ready for prime-time use. However, if you are brave enough to try working with development, see PGKitDevelopment for development information, including details of how to download and build the components from source.

For more details, including publications, see the main site page at http://proofgeneral.inf.ed.ac.uk/kit