Academic
Publications
Proof General / Eclipse: A Generic Interface for Interactive Proof

Proof General / Eclipse: A Generic Interface for Interactive Proof,Daniel Winterstein,David Aspinall,Christoph Lüth

Proof General / Eclipse: A Generic Interface for Interactive Proof   (Citations: 8)
BibTex | RIS | RefWorks Download
Abstract. This paper introduces PG/Eclipse; a sophisticated new in- terface for interactive theorem provers, ofiering users a rich set of proof development tools. It is based upon two complementary frameworks. The flrst is PG/Kit, a generic communication framework for connecting theorem provers and interfaces. PG/Kit should allow straightforward adaptation to most interactive theorem provers. Moreover, by separat- ing interface development from proof engine development, this framework should facilitate the development of both. The second is Eclipse, a so- phisticated open source framework for building IDEs. Eclipse is highly modular and extensible, making it a good platform for interface research. Using it has allowed us to provide a rich range of interface features. These frameworks correspond to the twin goals of this project: to deflne a clear separation between provers and interfaces, and to translate programming development tools to a theorem proving environment.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: