publication . Contribution for newspaper or weekly magazine . 2016

Coqoon - An IDE for Interactive Proof Development in Coq

Faithfull, Alexander; Bengtson, Jesper; Tassi, Enrico;
Open Access English
  • Published: 11 Apr 2016
  • Publisher: Springer
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 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 t...
Subjects
acm: Software_PROGRAMMINGLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Proof assistants, Coq, IDEs, Eclipse
Download from
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue