ITU

Coqoon - An IDE for Interactive Proof Development in Coq

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

Standard

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 chapterArticle in proceedingsResearchpeer-review

Harvard

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

APA

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. Lecture Notes in Computer Science Vol. 9636 https://doi.org/10.1007/978-3-662-49674-9_18

Vancouver

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). https://doi.org/10.1007/978-3-662-49674-9_18

Author

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

Bibtex

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

}

RIS

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 -

ID: 81631126