article

Coqoon

Authors:

Alexander Faithfull,

Jesper Bengtson,

Carst TankinkAuthors Info & Claims

International Journal on Software Tools for Technology Transfer (STTT), Volume 20, Issue 2

Pages 125 - 137

https://doi.org/10.1007/s10009-017-0457-2

Published: 01 April 2018 Publication History

Abstract

User interfaces for interactive proof assistants have always lagged behind those for mainstream programming languages. Whereas integrated development environments (IDEs) have support for features like project management, version control, dependency analysis and incremental project compilation, "IDE"s for proof assistants typically only operate on files in isolation, relying on external tools to integrate those files into larger projects. In this paper we present Coqoon, an IDE for Coq projects integrated into Eclipse. Coqoon manages proofs as projects rather than isolated source files and compiles these projects using the Eclipse common build system. Coqoon takes advantage of the latest features of Coq, including asynchronous and parallel processing of proofs and--when used together with a third-party OCaml extension for Eclipse--can even be used to work on large developments containing Coq plug-ins.

References

[1]

Aspinall, D.: Proof General: a generic tool for proof development. In: TACAS, vol. 1785 LNCS, pp. 38---42. Springer, (2000)

Digital Library

[2]

Aspinall, D., Lüth, C., Winterstein, D.: A framework for interactive proof. In: Calculemus/MKM, pp. 161---175, (2007)

Digital Library

[3]

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec$$^\sharp $$? programming system: an overview. In: CASSIS, pp. 49---69, (2005)

Digital Library

[4]

Barras, B., Tankink, C., Tassi, E.: Asynchronous processing of Coq documents: from the kernel up to the user interface. In: Proceedings of ITP, Nanjing, China, (August 2015)

[5]

Bengtson, Jesper: Jensen, Jonas Braband, Sieczkowski, Filip, Birkedal, Lars: Verifying object-oriented programs with higher-order separation logic in Coq. Lect Notes Comput Sci 6898, 22---38 (2011)

Digital Library

[6]

Boldo, S., Jourdan, J-H., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: ARITH, pp. 107---115. IEEE Computer Society, (2013)

Digital Library

[7]

Bros, N., Cerioli, R.: OcaIDE. Software, http://www.algo-prog.info/ocaide/

[8]

Charles, J., Kiniry, J.R.: A lightweight theorem prover interface for Eclipse. In: UITP Workshop proceedings, (2008)

[9]

Eclipse Foundation. EGit. Software, http://www.eclipse.org/egit/

[10]

Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns--Elements of Reusable Object-Oriented Software. Addison---Wesley, (1994). First edition, 20th printing

Digital Library

[11]

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O'Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: ITP, pp. 163---179. Springer, (2013)

Digital Library

[12]

Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)

Digital Library

[13]

Hales, Thomas C.: Dense Sphere Packings ---A Blueprint for Formal Proofs. Cambridge University Press, Cambridge (2012)

Digital Library

[14]

Harrison, J.: HOL Light: an overview. In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 60---66, (2009)

Digital Library

[15]

Jacobs, B., Piessens, F.: The VeriFast program verifier. CW Reports CW520, Department of Computer Science, K.U.Leuven, (August 2008)

[16]

Klein, Gerwin, Andronick, June, Elphinstone, Kevin, Murray, Toby C., Sewell, Thomas, Kolanski, Rafal, Heiser, Gernot: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)

Digital Library

[17]

Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR-16, pp. 348---370, (2010)

Digital Library

[18]

Magnusson, L., Nordström, B.: The ALF proof editor and its proof engine. In: Types for proofs and programs, pp. 213---237. Springer, (1994)

Digital Library

[19]

Mehnert, H.: Kopitiam: modular incremental interactive full functional static verification of Java code. In: NASA Formal Methods--Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18---20, 2011. Proceedings, pp. 518---524, (2011)

Digital Library

[20]

Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, (September 2007)

[21]

Ring, M., Lüth, C.: Collaborative interactive theorem proving with Clide. In: ITP, pp. 467---482. Springer, (2014)

[22]

The Coq Development Team. The Coq reference manual. http://coq.inria.fr/doc

[23]

Velykis, A.: Isabelle/Eclipse. Software, http://andriusvelykis.github.io/isabelle-eclipse

[24]

Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: ITP, vol. 8558 of LNCS, pp. 515---530. Springer, (2014)

[25]

Wenzel, M.: System description: Isabelle/jEdit in 2014. In: UITP, (2014)

Cited By

Hoang TSnook CDghaym DFathabadi AButler M(2022)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: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-26236-4_11
Brucker AWolff B(2019)Isabelle/DOF: Design and ImplementationSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_15(275-292)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_15
Mateescu R(2018)Recent advances in interactive and automated analysisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0477-y20:2(119-123)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0477-y

Index Terms

Coqoon

Index terms have been assigned to the content through auto-classification.

Recommendations

Coqoon
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 9636

User interfaces for interactive proof assistants have always lagged behind those for mainstream programming languages. Whereas integrated development environments--IDEs--have support for features like project management, version control, dependency ...
Java EE 5 Development using GlassFish Application Server: The complete guide to installing and configuring the GlassFish Application Server and developing ... 5 applications to be deployed to this server
Java EE 6 with GlassFish 3 Application Server

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal on Software Tools for Technology Transfer (STTT)

International Journal on Software Tools for Technology Transfer (STTT) Volume 20, Issue 2

April 2018

113 pages

ISSN:1433-2779

EISSN:1433-2787

Issue’s Table of Contents

Copyright © Copyright © 2018 Springer-Verlag GmbH Germany, part of Springer Nature.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 April 2018

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hoang TSnook CDghaym DFathabadi AButler M(2022)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: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-26236-4_11
Brucker AWolff B(2019)Isabelle/DOF: Design and ImplementationSoftware Engineering and Formal Methods10.1007/978-3-030-30446-1_15(275-292)Online publication date: 18-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-30446-1_15
Mateescu R(2018)Recent advances in interactive and automated analysisInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-017-0477-y20:2(119-123)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10009-017-0477-y

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents