D. Aspinall, Proof General: A Generic Tool for Proof Development Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference Held as Part of the European Joint Conferences on the Theory and Practice of Software Proceedings, Lecture Notes in Computer Science 1785, pp.38-4210, 2000.

B. Barras, C. Tankink, and &. Tassi, Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface, Interactive Theorem Proving -6th International Conference Proceedings, pp.51-6610, 2015.
DOI : 10.1007/978-3-319-22102-1_4
URL : https://hal.archives-ouvertes.fr/hal-01135919

J. Bengtson and &. Mehnert, Kopitiam?a unified IDE for developing formally verified Java programs, 2013.

Y. Bertot, The CtCoq System: Design and Architecture, Formal Aspects of Computing, vol.11, issue.3, pp.225-24310, 1999.
DOI : 10.1007/s001650050049
URL : https://hal.archives-ouvertes.fr/inria-00073145

D. Cervone, MathJax: A JavaScript display engine for mathematics that works in all browsers

A. Chlipala, Certified Programming with Dependent Types, 2011.

A. Faithfull, J. Bengtson, E. Tassi, and &. Tankink, Coqoon, Science + Business Media, pp.316-331978, 2016.
DOI : 10.1007/978-3-662-49674-9_18
URL : https://hal.archives-ouvertes.fr/hal-01410450

E. J. and G. Arias, jsCoq project page

E. J. and G. Arias, SerAPI: Machine-Friendly, Data-Centric Serialization for COQ Available at https://hal-mines-paristech.archives-ouvertes, 2016.

G. Gonthier, A. Mahboubi, and &. Tassi, A Small Scale Reflection Extension for the Coq system Available at https, 2008.

M. Haverbeke, Eloquent Javascript, 2011.

M. Haverbeke, CodeMirror is a versatile text editor implemented in JavaScript for the browser

I. Hickson, Web Worker Specification. https://www, 2015.

C. Kaliszyk, Web Interfaces for Proof Assistants, Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, pp.49-61, 2006.
DOI : 10.1016/j.entcs.2006.09.021

D. Ervin and K. , Literate Programming, The Computer Journal, vol.27, issue.2, pp.97-111, 1984.

F. Pérez, &. Brian, and E. Granger, IPython: A System for Interactive Scientific Computing, Computing in Science & Engineering, vol.9, issue.3, pp.21-29, 2007.
DOI : 10.1109/MCSE.2007.53

C. Benjamin, C. Pierce, M. Casinghino, M. Gaboardi, C. Greenberg et al., Software Foundations. Electronic textbook, 2015.

C. Pit and P. Courtieu, Company-Coq: Taking Proof General one step closer to a real IDE In: CoqPL'16: The Second International Workshop on Coq for PL, 2016.

V. Robert, PeaCoq is a web-based front-end to the Coq proof assistant. https://github

J. O. Smith and I. , Mathematics of the Discrete Fourier Transform (DFT): with Audio Applications Available at https://ccrma, 2007.

P. Steckler, Proof General with XML Protocol Support. https://github

C. Tankink, H. Geuvers, J. Mckinna, and &. Wiedijk, Proviola: A Tool for Proof Re-animation, In: Lecture Notes in Computer Science, pp.440-454978, 2010.
DOI : 10.1007/978-3-642-14128-7_37

J. Vouillon and &. Vincent-balat, From bytecode to JavaScript: the Js_of_ocaml compiler, Software: Practice and Experience, vol.26, issue.4, pp.951-972, 2014.
DOI : 10.1002/spe.2187
URL : https://hal.archives-ouvertes.fr/hal-00826786

M. Wenzel, PIDE as front-end technology for Coq, 2013.

M. Wenzel, Asynchronous User Interaction and Tool Integration in Isabelle/PIDE, Interactive Theorem Proving -5th International Conference, pp.515-530, 2014.
DOI : 10.1007/978-3-319-08970-6_33

W. Research-inc, Mathematica 8.0, 2010.

Z. Edward and . Yang, Logitext is an educational proof assistant for first-order classical logic using the sequent calculus, in the same tradition as Jape

B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, &. Viktor et al., Mtac: a monad for typed tactic programming in Coq, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, pp.87-100, 2013.