Coqoon - An IDE for Interactive Proof Development in Coq

Alexander Faithfull, Jesper Bengtson, Enrico Tassi

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


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
Publication date11 Apr 2016
ISBN (Print)978-3-662-49673-2
ISBN (Electronic)978-3-662-49674-9
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


ConferenceTools and Algorithms for the Construction and Analysis of Systems
LocationEindhoven University of Technology
Internet address
SeriesLecture Notes in Computer Science


  • Proof assistants
  • Coq
  • IDEs
  • Eclipse


Dive into the research topics of 'Coqoon - An IDE for Interactive Proof Development in Coq'. Together they form a unique fingerprint.

Cite this