References

  1. David Aspinall (2000): Proof General: A Generic Tool for Proof Development. In: Susanne Graf & Michael I. Schwartzbach: Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, Lecture Notes in Computer Science 1785. Springer, pp. 38–42, doi:10.1007/3-540-46419-0_3.
  2. Bruno Barras, Carst Tankink & Enrico Tassi (2015): Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface. In: Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, pp. 51–66, doi:10.1007/978-3-319-22102-1_4.
  3. Jesper Bengtson & Hannes Mehnert (2013): Kopitiam–a unified IDE for developing formally verified Java programs. Technical Report. IT University of Copenhagen.
  4. Yves Bertot (1999): The CtCoq System: Design and Architecture. Formal Asp. Comput. 11(3), pp. 225–243, doi:10.1007/s001650050049.
  5. Yves Bertot, Gilles Kahn & Laurent Théry (1994): Proof by Pointing. In: Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, pp. 141–160, doi:10.1007/3-540-57887-0_94.
  6. David Cervone: MathJax: A JavaScript display engine for mathematics that works in all browsers.. https://www.mathjax.org/.
  7. Adam Chlipala (2011): Certified Programming with Dependent Types. MIT Press. Available at http://adam.chlipala.net/cpdt/.
  8. Ryan Dahl: NodeJS. https://nodejs.org.
  9. Ecma International (2015): ECMAScript 2015 Language Specification, 6th edition. Ecma International, Geneva. Available at http://www.ecma-international.org/ecma-262/6.0/ECMA-262.pdf.
  10. Alexander Faithfull, Jesper Bengtson, Enrico Tassi & Carst Tankink (2016): Coqoon. In: Tools and Algorithms for the Construction and Analysis of Systems. Springer Science + Business Media, pp. 316–331, doi:10.1007/978-3-662-49674-9_18.
  11. Emilio Jesús Gallego Arias: jsCoq project page. https://github.com/ejgallego/jscoq.
  12. Emilio Jesús Gallego Arias (2016): SerAPI: Machine-Friendly, Data-Centric Serialization for COQ. Available at https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408. Working paper or preprint.
  13. Georges Gonthier, Assia Mahboubi & Enrico Tassi (2008): A Small Scale Reflection Extension for the Coq system. Research Report RR-6455. Available at https://hal.inria.fr/inria-00258384.
  14. Marijn Haverbeke (2011): Eloquent Javascript, 1st edition. No Starch Press. Available at http://eloquentjavascript.net/.
  15. Marijn Haverbeke: CodeMirror is a versatile text editor implemented in JavaScript for the browser.. https://codemirror.net/.
  16. Ian Hickson (2015): Web Worker Specification. https://www.w3.org/TR/workers.
  17. Cezary Kaliszyk (2007): Web Interfaces for Proof Assistants. Electronic Notes in Theoretical Computer Science 174(2), pp. 49 – 61, doi:10.1016/j.entcs.2006.09.021. Available at http://www.sciencedirect.com/science/article/pii/S1571066107001697. Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006).
  18. Donald Ervin Knuth (1984): Literate Programming. The Computer Journal 27(2), pp. 97–111, doi:10.1093/comjnl/27.2.97.
  19. Michael B. Monagan, Keith O. Geddes, K. Michael Heal, George Labahn, Stefan M. Vorkoetter, James McCarron & Paul DeMarco (2005): Maple 10 Programming Guide. Maplesoft, Waterloo ON, Canada.
  20. Fernando Pérez & Brian E. Granger (2007): IPython: A System for Interactive Scientific Computing. Computing in Science & Engineering 9(3), pp. 21–29, doi:10.1109/mcse.2007.53. http://ipython.org.
  21. Benjamin C. Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cǎtǎlin Hriţcu, Vilhelm Sjoberg & Brent Yorgey (2015): Software Foundations. Electronic textbook. http://www.cis.upenn.edu/~bcpierce/sf.
  22. Clément Pit-Claudel & Pierre Courtieu (2016): Company-Coq: Taking Proof General one step closer to a real IDE. In: CoqPL'16: The Second International Workshop on Coq for PL, doi:10.5281/zenodo.44331. Available at http://hdl.handle.net/1721.1/101149.
  23. Valentin Robert: PeaCoq is a web-based front-end to the Coq proof assistant.. https://github.com/Ptival/PeaCoq.
  24. Benoît Rognier, Guillaume Duhamel, Romain Guillot & Jérémie Maquet: Edukera. http://edukera.com.
  25. Julius Orion Smith III (2007): Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications, 2nd edition. W3K Publishing. Available at https://ccrma.stanford.edu/~jos/mdft/.
  26. Paul Steckler: Proof General with XML Protocol Support. https://github.com/psteckler/ProofGeneral.
  27. Carst Tankink, Herman Geuvers, James McKinna & Freek Wiedijk (2010): Proviola: A Tool for Proof Re-animation. In: Lecture Notes in Computer Science. Springer Science + Business Media, pp. 440–454, doi:10.1007/978-3-642-14128-7_37.
  28. The Coq development team (2016): The Coq proof assistant reference manual. LogiCal Project. Available at http://coq.inria.fr. Version 8.5pl1.
  29. Jérôme Vouillon & Vincent Balat (2014): From bytecode to JavaScript: the Js_of_ocaml compiler. Softw., Pract. Exper. 44(8), pp. 951–972, doi:10.1002/spe.2187.
  30. Makarius Wenzel (2013): PIDE as front-end technology for Coq. CoRR abs/1304.6626. Available at http://arxiv.org/abs/1304.6626.
  31. Makarius Wenzel (2014): Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. In: Gerwin Klein & Ruben Gamboa: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, Lecture Notes in Computer Science 8558. Springer, pp. 515–530, doi:10.1007/978-3-319-08970-6_33.
  32. whitequark: ppx_deriving_yojson. https://github.com/whitequark/ppx_deriving_yojson.
  33. Steven Wittens: mathbox: Presentation-quality WebGL math graphing. https://gitgud.io/unconed/mathbox.
  34. Wolfram Research Inc. (2010): Mathematica 8.0. Available at http://www.wolfram.com.
  35. Edward Z. Yang: Logitext is an educational proof assistant for first-order classical logic using the sequent calculus, in the same tradition as Jape, Pandora, Panda and Yoda.. http://logitext.mit.edu/main.
  36. Alon Zakai: emscripten. http://emscripten.org.
  37. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski & Viktor Vafeiadis (2013): Mtac: a monad for typed tactic programming in Coq. In: Greg Morrisett & Tarmo Uustalu: ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013. ACM, pp. 87–100, doi:10.1145/2500365.2500579.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org