Coqoon - An IDE for Interactive Proof Development in Coq

Alexander Faithfull; Jesper Bengtson; Enrico Tassi

doi:10.1007/978-3-662-49674-9_18

Coqoon - An IDE for Interactive Proof Development in Coq

Alexander Faithfull, Jesper Bengtson, Enrico Tassi

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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.

Original language	English
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
Number of pages	15
Publisher	Springer
Publication date	11 Apr 2016
Pages	316-331
ISBN (Print)	978-3-662-49673-2
ISBN (Electronic)	978-3-662-49674-9
DOIs	https://doi.org/10.1007/978-3-662-49674-9_18
Publication status	Published - 11 Apr 2016
Event	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

Conference

Conference	Tools and Algorithms for the Construction and Analysis of Systems
Number	22
Location	Eindhoven University of Technology
Country/Territory	Netherlands
City	Eindhoven
Period	02/04/2016 → 07/04/2016
Internet address	http://www.etaps.org/2016/tacas

Series	Lecture Notes in Computer Science
Volume	9636
ISSN	0302-9743

Keywords

Proof assistants
Coq
IDEs
Eclipse

Access to Document

10.1007/978-3-662-49674-9_18

mainFinal published version, 760 KB

Cite this

Faithfull, A., Bengtson, J., & Tassi, E. (2016). Coqoon - An IDE for Interactive Proof Development in Coq. In 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 (pp. 316-331). Springer. https://doi.org/10.1007/978-3-662-49674-9_18

Faithfull, Alexander ; Bengtson, Jesper ; Tassi, Enrico. / Coqoon - An IDE for Interactive Proof Development in Coq. 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. Springer, 2016. pp. 316-331 (Lecture Notes in Computer Science, Vol. 9636).

@inproceedings{6b9ab6dfa5d346129118048708e55ab6,

title = "Coqoon - An IDE for Interactive Proof Development in Coq",

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.",

keywords = "Proof assistants, Coq, IDEs, Eclipse",

author = "Alexander Faithfull and Jesper Bengtson and Enrico Tassi",

year = "2016",

month = apr,

day = "11",

doi = "10.1007/978-3-662-49674-9_18",

language = "English",

isbn = "978-3-662-49673-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "316--331",

booktitle = "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",

address = "Germany",

note = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS ; Conference date: 02-04-2016 Through 07-04-2016",

url = "http://www.etaps.org/2016/tacas",

}

Faithfull, A, Bengtson, J & Tassi, E 2016, Coqoon - An IDE for Interactive Proof Development in Coq. in 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. Springer, Lecture Notes in Computer Science, vol. 9636, pp. 316-331, Tools and Algorithms for the Construction and Analysis of Systems, Eindhoven, Netherlands, 02/04/2016. https://doi.org/10.1007/978-3-662-49674-9_18

Coqoon - An IDE for Interactive Proof Development in Coq. / Faithfull, Alexander; Bengtson, Jesper; Tassi, Enrico.
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. Springer, 2016. p. 316-331 (Lecture Notes in Computer Science, Vol. 9636).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Coqoon - An IDE for Interactive Proof Development in Coq

AU - Faithfull, Alexander

AU - Bengtson, Jesper

AU - Tassi, Enrico

N1 - Conference code: 22

PY - 2016/4/11

Y1 - 2016/4/11

N2 - 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.

AB - 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.

KW - Proof assistants

KW - Coq

KW - IDEs

KW - Eclipse

U2 - 10.1007/978-3-662-49674-9_18

DO - 10.1007/978-3-662-49674-9_18

M3 - Article in proceedings

SN - 978-3-662-49673-2

T3 - Lecture Notes in Computer Science

SP - 316

EP - 331

BT - 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

PB - Springer

T2 - Tools and Algorithms for the Construction and Analysis of Systems

Y2 - 2 April 2016 through 7 April 2016

ER -

Faithfull A, Bengtson J, Tassi E. Coqoon - An IDE for Interactive Proof Development in Coq. In 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. Springer. 2016. p. 316-331. (Lecture Notes in Computer Science, Vol. 9636). doi: 10.1007/978-3-662-49674-9_18

Coqoon - An IDE for Interactive Proof Development in Coq

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this