Skip to main content
SpringerLink
Log in

CoqPIE: An IDE Aimed at Improving Proof Development Productivity

(Rough Diamond)

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9807))

Included in the following conference series:

Abstract

In this paper we present CoqPIE(CoqPIE is available for download at http://github.com/kendroe/CoqPIE), a new development environment for Coq which delivers editing functionality centered around common prover usage workflow not found in existing tools. The main contributions of CoqPIE build from having an integrated parser for both Coq source and for prover output. The primary novelty is not the parser but how it is used: CoqPIE includes tools to carry out complex editing functions such as lemma extraction and replay. In proof replay for example both new and old outputs of the proof script are parsed into ASTs. These ASTs allow replay to do updates such as fixing hypothesis references.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A couple of type checking errors showed up in CoqPIE but not when compiling outside of CoqPIE. We are still working to find the source of these errors.

References

  1. Coq 8.5 beta release. https://coq.inria.fr/news/123.html. Accessed 20 Mar 2015

  2. Coqoon home page. https://itu.dk/research/tomeso/coqoon/. Accessed 19 Mar 2015

  3. MIT proofs page. http://proofs.csail.mit.edu/. Accessed 19 Mar 2015

  4. Peacoq home page. http://goto.ucsd.edu/peacoq/. Accessed 19 Mar 2015

  5. Proof general. http://proofgeneral.inf.ed.ac.uk/. Accessed 20 Mar 2015

  6. Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics: applications and extraction for Coq and Mizar. In: AISC/MKM/Calculemus, pp. 1–16 (2012)

    Google Scholar 

  7. Ayache, N.: Combining the Coq proof assistant with first-order decision procedures (2006)

    Google Scholar 

  8. Barras, B., Tankink, C., Tassi, E.: Asynchronous processing of Coq documents: from the kernel up to the user interface. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 51–66. Springer International Publishing, Switzerland (2015)

    Google Scholar 

  9. Bertot, J., Bertot, Y.: CtCoq: a system presentation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 231–234. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  10. Bertot, Y.: Pcoq: a graphical user-interface for Coq. https://www-sop.inria.fr/lemme/pcoq/

  11. Bertot, Y.: The CtCoq system: design and architecture. Formal Aspect Comput. 11(3), 225–243 (1999)

    Article  MathSciNet  Google Scholar 

  12. Bertot, Y., Kahn, G., Théry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 141–160. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  13. Boite, O.: Proof reuse with extended inductive types. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 50–65. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  14. Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: 14th ICFP (2009)

    Google Scholar 

  15. Faithfull, A., Bengtson, J., Tassi, E., Tankink, C.: Coqoon: an IDE for interactive proof development in Coq. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 316–331. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_18

    Chapter  Google Scholar 

  16. Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2014)

    Google Scholar 

  17. Hasker, R.: The replay of program derivations. Ph.D. thesis, University of Illinois at Urbana-Champaign (1995)

    Google Scholar 

  18. Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS, vol. 6824, pp. 260–275. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 374–389. Springer, Heidelberg (2014)

    Google Scholar 

  20. Pierce, B.C., Casinghino, C., Gaboardi, M., Greenberg, M., Hritcu, C., Sjoberg, V., Yorgey, B.: Software foundations. https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

  21. Pit-Claudel, C., Courtieu, P.: Company-Coq: taking proof general one step closer to a real IDE. In: Coq PL (2016)

    Google Scholar 

  22. Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: UITP (1998)

    Google Scholar 

  23. Tankink, C.: PIDE for asynchronous interation with Coq. http://arxiv.org/pdf/1410.8221.pdf

  24. Tankink, C.: Proof in context - web editing with rich modeless contextual feedback. In: 10th International Workshop on User Interfaces for Theorem Provers, pp. 42–56 (2012)

    Google Scholar 

  25. Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: a tool for proof re-animation. In: 9th International Conference on Mathematical Knowledge Management (2010)

    Google Scholar 

  26. Vijayaraghavan, M., Chlipala, A., Arvind, Dave, N.: Modular deductive verification of multiprocessor hardware designs. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 109–127. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  27. Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515–530. Springer, Heidelberg (2014)

    Google Scholar 

  28. Wenzel, M.: Isabelle/jedit (2014). http://isabelle.in.tum.de/dist/doc/jedit.pdf. Accessed 19 Mar 2015

Download references

Acknowledgements

The authors would like to thank Gregory Malecha, Valentin Robert and Jesper Bengston for their feedback.

Author information

Authors and Affiliations

  1. The Johns Hopkins University, Baltimore, USA

    Kenneth Roe & Scott Smith

Authors
  1. Kenneth Roe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Scott Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kenneth Roe .

Editor information

Editors and Affiliations

  1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Jasmin Christian Blanchette

  2. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Stephan Merz

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Roe, K., Smith, S. (2016). CoqPIE: An IDE Aimed at Improving Proof Development Productivity. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-43144-4_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-43143-7

  • Online ISBN: 978-3-319-43144-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation