Proof General in Eclipse: System and Architecture Overview

David Aspinall, Daniel Winterstein, Christoph Lüth, Ahsan Fayyaz

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

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationeclipse '06 Proceedings of the 2006 OOPSLA workshop on eclipse technology eXchange
Place of PublicationNew York, NY, USA
Number of pages5
ISBN (Print)1-59593-621-1
Publication statusPublished - 2006


Dive into the research topics of 'Proof General in Eclipse: System and Architecture Overview'. Together they form a unique fingerprint.

Cite this