Protocols for Interactive e-Proof

Research output: Chapter in Book/Report/Conference proceedingConference contribution


I motivate and describe work-in-progress on Proof General Kit . an evolution of the Proof General project. Proof General Kit introduces a new architecture for Proof General. Instead of the present monolithic implementation in Emacs Lisp, where each proof assistant is connected through a separate customization, Proof General will become a collection of pluggable communicating components using a standard protocol. The Kit is centred around this protocol for interactive electronic proof, dubbed PGIP. The design of PGIP has been influenced by the generic mechanisms that Proof General presently uses to communicate with various interactive proof assistants. PGIP is a rationalization of these mechanisms, and will be proposed as an open standard for future proof assistants to support. Messages in PGIP are small XML documents. PGIP comes with an associated markup language, PGML, for representing structural aspects of concrete syntax
Original languageEnglish
Title of host publicationSupplemental proceedings of the 13th international conference on theorem proving in higher order logics (TPHOLs 2000)
Number of pages8
Publication statusPublished - Jul 2000


Dive into the research topics of 'Protocols for Interactive e-Proof'. Together they form a unique fingerprint.

Cite this