@inproceedings(DBLP:conf/tacas/Aspinall00,
 author       = {David Aspinall},
 year         = {2000},
 title        = {Proof General: {A} Generic Tool for Proof Development},
 editor       = {Susanne Graf and Michael~I. Schwartzbach},
 booktitle    = {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},
 series       = {Lecture Notes in Computer Science},
 volume       = {1785},
 publisher    = {Springer},
 pages        = {38--42},
 doi          = {10.1007/3-540-46419-0\_3},
)
@inproceedings(DBLP:conf/itp/BarrasTT15,
 author       = {Bruno Barras and Carst Tankink and Enrico Tassi},
 year         = {2015},
 title        = {Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface},
 booktitle    = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015, Proceedings},
 pages        = {51--66},
 doi          = {10.1007/978-3-319-22102-1\_4},
)
@techreport(bengtson2013kopitiam,
 author       = {Jesper Bengtson and Hannes Mehnert},
 year         = {2013},
 title        = {Kopitiam--a unified IDE for developing formally verified Java programs},
 type         = {Technical Report},
 institution  = {IT University of Copenhagen},
)
@article(DBLP:journals/fac/Bertot99,
 author       = {Yves Bertot},
 year         = {1999},
 title        = {The CtCoq System: Design and Architecture},
 journal      = {Formal Asp. Comput.},
 volume       = {11},
 number       = {3},
 pages        = {225--243},
 doi          = {10.1007/s001650050049},
)
@inproceedings(DBLP:conf/tacs/BertotKT94,
 author       = {Yves Bertot and Gilles Kahn and Laurent Th{\'{e}}ry},
 year         = {1994},
 title        = {Proof by Pointing},
 booktitle    = {Theoretical Aspects of Computer Software, International Conference {TACS} '94, Sendai, Japan, April 19-22, 1994, Proceedings},
 pages        = {141--160},
 doi          = {10.1007/3-540-57887-0\_94},
)
@misc(mathjax,
 author       = {David Cervone},
 title        = {MathJax: A JavaScript display engine for mathematics that works in all browsers.},
 howpublished = {\url{https://www.mathjax.org/}},
)
@book(chlipalacpdt2011,
 author       = {Adam Chlipala},
 year         = {2011},
 title        = {Certified Programming with Dependent Types},
 publisher    = {MIT Press},
 url          = {{http://adam.chlipala.net/cpdt/}},
)
@misc(nodejs,
 author       = {Ryan Dahl},
 title        = {NodeJS},
 howpublished = {\url{https://nodejs.org}},
)
@book(EcmaScript:15,
 author       = {{Ecma International}},
 year         = {2015},
 title        = {{ECMAScript 2015 Language Specification}},
 edition      = {6th},
 publisher    = {{Ecma International}},
 address      = {Geneva},
 url          = {http://www.ecma-international.org/ecma-262/6.0/ECMA-262.pdf},
)
@incollection(Faithfull_2016,
 author       = {Alexander Faithfull and Jesper Bengtson and Enrico Tassi and Carst Tankink},
 year         = {2016},
 title        = {Coqoon},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
 publisher    = {Springer Science $+$ Business Media},
 pages        = {316--331},
 doi          = {10.1007/978-3-662-49674-9\_18},
)
@misc(jscoq-github,
 author       = {Gallego~Arias, Emilio~Jes\'{u}s},
 title        = {jsCoq project page},
 howpublished = {\url{https://github.com/ejgallego/jscoq}},
)
@unpublished(gallegoarias:hal-01384408,
 author       = {Gallego~Arias, Emilio~Jes{\'u}s},
 year         = {2016},
 title        = {{SerAPI: Machine-Friendly, Data-Centric Serialization for COQ}},
 url          = {https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408},
 note         = {Working paper or preprint},
)
@techreport(gonthier:inria-00258384,
 author       = {Georges Gonthier and Assia Mahboubi and Enrico Tassi},
 year         = {2008},
 title        = {{A Small Scale Reflection Extension for the Coq system}},
 type         = {Research Report},
 number       = {RR-6455},
 url          = {https://hal.inria.fr/inria-00258384},
)
@book(eloquent-js,
 author       = {Marijn Haverbeke},
 year         = {2011},
 title        = {Eloquent Javascript},
 edition      = {1st},
 publisher    = {No Starch Press},
 url          = {http://eloquentjavascript.net/},
)
@misc(codemirror,
 author       = {Marijn Haverbeke},
 title        = {CodeMirror is a versatile text editor implemented in JavaScript for the browser.},
 howpublished = {\url{https://codemirror.net/}},
)
@misc(web-workers,
 author       = {Ian Hickson},
 year         = {2015},
 title        = {Web Worker Specification},
 howpublished = {\url{https://www.w3.org/TR/workers}},
)
@article(Kaliszyk200749,
 author       = {Cezary Kaliszyk},
 year         = {2007},
 title        = {Web Interfaces for Proof Assistants},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {174},
 number       = {2},
 pages        = {49 -- 61},
 doi          = {10.1016/j.entcs.2006.09.021},
 url          = {http://www.sciencedirect.com/science/article/pii/S1571066107001697},
 note         = {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)},
)
@article(knuth1984literate,
 author       = {Donald~Ervin Knuth},
 year         = {1984},
 title        = {Literate Programming},
 journal      = {The Computer Journal},
 volume       = {27},
 number       = {2},
 pages        = {97--111},
 doi          = {10.1093/comjnl/27.2.97},
)
@book(Maple10,
 author       = {Michael~B. Monagan and Keith~O. Geddes and K.~Michael Heal and George Labahn and Stefan~M. Vorkoetter and James McCarron and Paul DeMarco},
 year         = {2005},
 title        = {Maple~10 Programming Guide},
 publisher    = {Maplesoft},
 address      = {Waterloo ON, Canada},
)
@article(PER-GRA:2007,
 author       = {Fernando P\'erez and Brian~E. Granger},
 year         = {2007},
 title        = {{IPython}: A System for Interactive Scientific Computing},
 journal      = {Computing in Science {\&} Engineering},
 volume       = {9},
 number       = {3},
 pages        = {21--29},
 doi          = {10.1109/mcse.2007.53},
 note         = {\url{http://ipython.org}},
)
@book(Pierce:SF,
 author       = {Benjamin~C. Pierce and Chris Casinghino and Marco Gaboardi and Michael Greenberg and Hri\c{t}cu, C\v{a}t\v{a}lin and Vilhelm Sjoberg and Brent Yorgey},
 year         = {2015},
 title        = {Software Foundations},
 publisher    = {Electronic textbook},
 note         = {\url{http://www.cis.upenn.edu/~bcpierce/sf}},
)
@inproceedings(CompanyCoq2016,
 author       = {Pit-Claudel, Cl\IeC{\'e}ment and Pierre Courtieu},
 year         = {2016},
 title        = {Company-Coq: Taking Proof General one step closer to a real IDE},
 booktitle    = {CoqPL'16: The Second International Workshop on Coq for PL},
 doi          = {10.5281/zenodo.44331},
 url          = {http://hdl.handle.net/1721.1/101149},
)
@misc(peacoq,
 author       = {Valentin Robert},
 title        = {PeaCoq is a web-based front-end to the Coq proof assistant.},
 howpublished = {\url{https://github.com/Ptival/PeaCoq}},
)
@misc(edukera,
 author       = {Beno\^{i}t Rognier and Guillaume Duhamel and Romain Guillot and J\'{e}r\'{e}mie Maquet},
 title        = {Edukera},
 howpublished = {\url{http://edukera.com}},
)
@book(jos:mdft,
 author       = {Smith~III, Julius~Orion},
 year         = {2007},
 title        = {Mathematics of the Discrete Fourier Transform ({DFT}): with Audio Applications},
 edition      = {2nd},
 publisher    = {W3K Publishing},
 url          = {https://ccrma.stanford.edu/~jos/mdft/},
)
@misc(pg-xml,
 author       = {Paul Steckler},
 title        = {Proof General with XML Protocol Support},
 howpublished = {\url{https://github.com/psteckler/ProofGeneral}},
)
@incollection(Tankink_2010,
 author       = {Carst Tankink and Herman Geuvers and James McKinna and Freek Wiedijk},
 year         = {2010},
 title        = {Proviola: A Tool for Proof Re-animation},
 booktitle    = {Lecture Notes in Computer Science},
 publisher    = {Springer Science $+$ Business Media},
 pages        = {440--454},
 doi          = {10.1007/978-3-642-14128-7\_37},
)
@manual(Coq:manual,
 author       = {{C}oq~development team, The},
 year         = {2016},
 title        = {The {C}oq proof assistant reference manual},
 organization = {LogiCal Project},
 url          = {http://coq.inria.fr},
 note         = {Version 8.5pl1},
)
@article(DBLP:journals/spe/VouillonB14,
 author       = {J{\'{e}}r{\^{o}}me Vouillon and Vincent Balat},
 year         = {2014},
 title        = {From bytecode to JavaScript: the Js{\_}of{\_}ocaml compiler},
 journal      = {Softw., Pract. Exper.},
 volume       = {44},
 number       = {8},
 pages        = {951--972},
 doi          = {10.1002/spe.2187},
)
@article(DBLP:journals/corr/abs-1304-6626,
 author       = {Makarius Wenzel},
 year         = {2013},
 title        = {{PIDE} as front-end technology for Coq},
 journal      = {CoRR},
 volume       = {abs/1304.6626},
 url          = {http://arxiv.org/abs/1304.6626},
)
@inproceedings(DBLP:conf/itp/Wenzel14,
 author       = {Makarius Wenzel},
 year         = {2014},
 title        = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},
 editor       = {Gerwin Klein and Ruben Gamboa},
 booktitle    = {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},
 series       = {Lecture Notes in Computer Science},
 volume       = {8558},
 publisher    = {Springer},
 pages        = {515--530},
 doi          = {10.1007/978-3-319-08970-6\_33},
)
@misc(ppx-yojson,
 author       = {whitequark},
 title        = {ppx\_deriving\_yojson},
 howpublished = {\url{https://github.com/whitequark/ppx_deriving_yojson}},
)
@misc(mathbox,
 author       = {Steven Wittens},
 title        = {mathbox: Presentation-quality WebGL math graphing},
 howpublished = {\url{https://gitgud.io/unconed/mathbox}},
)
@manual(ram2010,
 author       = {{Wolfram Research Inc.}},
 year         = {2010},
 title        = {Mathematica 8.0},
 url          = {http://www.wolfram.com},
)
@misc(logitext,
 author       = {Edward~Z. Yang},
 title        = {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.},
 howpublished = {\url{http://logitext.mit.edu/main}},
)
@misc(emscripten,
 author       = {Alon Zakai},
 title        = {emscripten},
 howpublished = {\url{http://emscripten.org}},
)
@inproceedings(DBLP:conf/icfp/ZilianiDKNV13,
 author       = {Beta Ziliani and Derek Dreyer and Neelakantan~R. Krishnaswami and Aleksandar Nanevski and Viktor Vafeiadis},
 year         = {2013},
 title        = {Mtac: a monad for typed tactic programming in {C}oq},
 editor       = {Greg Morrisett and Tarmo Uustalu},
 booktitle    = {{ACM} {SIGPLAN} International Conference on Functional Programming, ICFP'13, Boston, MA, {USA} - September 25 - 27, 2013},
 publisher    = {{ACM}},
 pages        = {87--100},
 doi          = {10.1145/2500365.2500579},
)