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 developments 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 plugins.
Title of host publication
22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings : TACAS 2016: Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems - Eindhoven University of Technology, Eindhoven, Netherlands Duration: 2 Apr 2016 → 7 Apr 2016 Conference number: 22 http://www.etaps.org/2016/tacas
Tools and Algorithms for the Construction and Analysis of Systems
This page is printed from https://en.itu.dk/research/portalplaceholder?layoutfraction=top&langRef=https://pure.itu.dk/portal/da/organisations/computer-science(768f3a75-8ff6-46cf-8ab0-c09d1057ec3b)/publications.html?filter=research&page=2