skip to main content
10.1145/1188835.1188845acmotherconferencesArticle/Chapter ViewAbstractPublication PagessplashConference Proceedingsconference-collections
Article

Proof general in Eclipse: system and architecture overview

Published: 22 October 2006 Publication History

Abstract

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.

References

[1]
D. Aspinall and C. Lüth. Commentary on PGIP. http://proofgeneral.inf.ed.ac.uk/kit/, 2006.
[2]
D. Aspinall, C. Lüth, and D. Winterstein. Parsing, editing, proving: The PGIP display protocol. In User Interfaces for Theorem Provers UITP'05, Apr. 2005.
[3]
D. Aspinall, C. Lüth, and B. Wolff. Assisted proof document authoring. In Proc. Intl. conf. Mathematical Knowledge Management 2005, LNAI 3863. Springer, 2005.
[4]
B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge, 2005.
[5]
Y. Bertot and L. Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7):161--194, Feb. 1998.
[6]
G. Gonthier. A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge, 2004. http://research. microsoft.com/~gonthier/4colproof.pdf.
[7]
T. C. Hales. The Flyspeck project page. http://www.math.pitt.edu/~thales/flyspeck/index.html.
[8]
R. Kaivola and K. R. Kohatsu. Proof engineering in the large: formal verification of Pentium 4 floating-point divider. STTT, 4(3):323--334, 2003.
[9]
M. Kohlhase. OMDoc: An Open Markup Format for Mathematical Documents. LNAI 4180. Springer, 2006.
[10]
TeXmacs. Web page, 2006. http://www.texmacs.org/.
[11]
D. von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173--1214, 2001.
[12]
Mathematical markup language (MathML). W3C Recommendation, 1999.
[13]
M. Wenzel. Isabelle/Isar --- a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München, 2001.

Cited By

View all
  • (2023)Building an Extensible Textual Framework for the Rodin PlatformSoftware Engineering and Formal Methods. SEFM 2022 Collocated Workshops10.1007/978-3-031-26236-4_11(132-147)Online publication date: 11-Feb-2023
  • (2012)Engineering the Prover InterfaceElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2012.06.002285:C(3-16)Online publication date: 19-Sep-2012
  • (2010)Towards an industrial grade IVE for Java and next generation research platform for JMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-010-0164-812:6(429-446)Online publication date: 15-Jun-2010
  • Show More Cited By

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences
eclipse '06: Proceedings of the 2006 OOPSLA workshop on eclipse technology eXchange
October 2006
93 pages
ISBN:1595936211
DOI:10.1145/1188835
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

  • IBM: IBM

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 October 2006

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Acceptance Rates

eclipse '06 Paper Acceptance Rate 17 of 30 submissions, 57%;
Overall Acceptance Rate 38 of 79 submissions, 48%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 11 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Building an Extensible Textual Framework for the Rodin PlatformSoftware Engineering and Formal Methods. SEFM 2022 Collocated Workshops10.1007/978-3-031-26236-4_11(132-147)Online publication date: 11-Feb-2023
  • (2012)Engineering the Prover InterfaceElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2012.06.002285:C(3-16)Online publication date: 19-Sep-2012
  • (2010)Towards an industrial grade IVE for Java and next generation research platform for JMLInternational Journal on Software Tools for Technology Transfer10.1007/s10009-010-0164-812:6(429-446)Online publication date: 15-Jun-2010
  • (2009)Managing Proof Documents for Asynchronous ProcessingElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2008.12.097226(49-66)Online publication date: 1-Jan-2009
  • (2005)Assisted proof document authoringProceedings of the 4th international conference on Mathematical Knowledge Management10.1007/11618027_5(65-80)Online publication date: 15-Jul-2005

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media