nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

02.05.2017 | TACAS 2016

Coqoon

An IDE for interactive proof development in Coq

verfasst von: Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Recent advances in interactive and automated analysis

Nächster Artikel The Tinker tool for graphical tactic development

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

The interested reader can browse it online: http://math-comp.github.io/math-comp/htmldoc/libgraph.html.

http://proofgeneral.inf.ed.ac.uk/eclipse/products/.

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

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

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

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)

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)MathSciNetCrossRef

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)

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

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

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

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)

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)MATH

13.

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

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)

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)CrossRef

17.

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

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)

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)

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)

Titel: Coqoon
An IDE for interactive proof development in Coq
verfasst von: Alexander Faithfull
Jesper Bengtson
Enrico Tassi
Carst Tankink
Publikationsdatum: 02.05.2017
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 2/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-017-0457-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 2/2018

Recent advances in interactive and automated analysis

The Tinker tool for graphical tactic development

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives

Multi-core symbolic bisimulation minimisation

Automated translation of VDM to JML-annotated Java