Coqoon - An IDE for Interactive Proof Development in Coq

Alexander Faithfull, Jesper Bengtson, Enrico Tassi

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

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 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.
OriginalsprogEngelsk
Titel22nd 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
Antal sider15
ForlagSpringer
Publikationsdato11 apr. 2016
Sider316-331
ISBN (Trykt)978-3-662-49673-2
ISBN (Elektronisk)978-3-662-49674-9
DOI
StatusUdgivet - 11 apr. 2016
BegivenhedTools and Algorithms for the Construction and Analysis of Systems - Eindhoven University of Technology, Eindhoven, Holland
Varighed: 2 apr. 20167 apr. 2016
Konferencens nummer: 22
http://www.etaps.org/2016/tacas

Konference

KonferenceTools and Algorithms for the Construction and Analysis of Systems
Nummer22
LokationEindhoven University of Technology
Land/OmrådeHolland
ByEindhoven
Periode02/04/201607/04/2016
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind9636
ISSN0302-9743

Emneord

  • Proof assistants
  • Coq
  • IDEs
  • Eclipse

Fingeraftryk

Dyk ned i forskningsemnerne om 'Coqoon - An IDE for Interactive Proof Development in Coq'. Sammen danner de et unikt fingeraftryk.

Citationsformater