ITU

Coqoon - An IDE for Interactive Proof Development in Coq

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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.
Original languageEnglish
Title of host publication22nd 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
Number of pages15
PublisherSpringer
Publication date11 Apr 2016
Pages316-331
ISBN (Print)978-3-662-49673-2
ISBN (Electronic)978-3-662-49674-9
DOIs
Publication statusPublished - 11 Apr 2016
EventTools and Algorithms for the Construction and Analysis of Systems - Eindhoven University of Technology, Eindhoven, Netherlands
Duration: 2 Apr 20167 Apr 2016
Conference number: 22
http://www.etaps.org/2016/tacas

Conference

ConferenceTools and Algorithms for the Construction and Analysis of Systems
Nummer22
LocationEindhoven University of Technology
LandNetherlands
ByEindhoven
Periode02/04/201607/04/2016
Internetadresse
SeriesLecture Notes in Computer Science
Volume9636
ISSN0302-9743
Close

    Research areas

  • Proof assistants, Coq, IDEs, Eclipse

Downloads

No data available

ID: 81631126