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 in-cremental 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.
Type de document :
Communication dans un congrès
TACAS, Apr 2016, Eindhoven, Netherlands. LNCS
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01242295
Contributeur : Enrico Tassi <>
Soumis le : vendredi 11 décembre 2015 - 17:23:41
Dernière modification le : lundi 9 avril 2018 - 12:20:04
Document(s) archivé(s) le : samedi 29 avril 2017 - 12:07:33

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01242295, version 1

Collections

Citation

Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink. Coqoon An IDE for interactive proof development in Coq. TACAS, Apr 2016, Eindhoven, Netherlands. LNCS. 〈hal-01242295〉

Partager

Métriques

Consultations de la notice

250

Téléchargements de fichiers

473