Publikation
Proof General in Eclipse
David Aspinall; Christoph Lüth; Daniel Winterstein; Ahsan Fayyaz
In: Eclipse Technology eXchange ETX'06. Eclipse Technology Exchange Workshop (ETX-06), ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, located at OOPSLA 2006, October 22-26, Portland, OR, USA, ACM Press, 2006.
Zusammenfassung
Interactive theorem proving is the art of constructing electronic
proofs. Proof development, based around a proof script, has much in
common with program development, based around a program text. Proof
developers use rather primitive tools for developing and
manipulating proof scripts at present. The Proof General project
aims at to change this, by providing powerful generic tools and
interfaces. The flagship tool is our Eclipse plugin, which brings
the features of a industrial-strength IDE to theorem proving for the
first time. In this paper we give an overview of the Eclipse plugin
and its underlying architecture.