Towards Merging PlatΩ and PGIP

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


The PGIP protocol is a standard, abstract interface protocol to connect theorem provers with user interfaces. Interaction in PGIP is based on ASCII-text input and a single focus point-of-control, which indicates a linear position in the input that has been checked thus far. This fits many interactive theorem provers whose interaction model stems from command-line interpreters. PlatΩ, on the other hand, is a system with a new protocol tailored to transparently integrate theorem provers into text editors like that support semi-structured XML input files and multiple foci of attention. In this paper we extend the PGIP protocol and middleware broker to support the functionalities provided by PlatΩ and beyond. More specifically, we extend PGIP (i) to support multiple foci in provers; (ii) to display semi-structured documents; (iii) to combine prover updates with user edits; (iv) to support context-sensitive service menus, and (v) to allow multiple displays. As well as supporting , the extended PGIP protocol in principle can support other editors such as OpenOffice, Word 2007 and graph viewers; we hope it will also provide guidance for extending provers to handle multiple foci.
Original languageEnglish
Title of host publicationProceedings of the 8th International Workshop on User Interfaces for Theorem Provers (UITP 2008)
Number of pages18
Publication statusPublished - 9 Jan 2009


Dive into the research topics of 'Towards Merging PlatΩ and PGIP'. Together they form a unique fingerprint.

Cite this