{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:48Z","timestamp":1774837968583,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,5,2]],"date-time":"2017-05-02T00:00:00Z","timestamp":1493683200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10009-017-0457-2","type":"journal-article","created":{"date-parts":[[2017,5,2]],"date-time":"2017-05-02T01:49:38Z","timestamp":1493689778000},"page":"125-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Coqoon"],"prefix":"10.1007","volume":"20","author":[{"given":"Alexander","family":"Faithfull","sequence":"first","affiliation":[]},{"given":"Jesper","family":"Bengtson","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]},{"given":"Carst","family":"Tankink","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,2]]},"reference":[{"key":"457_CR1","doi-asserted-by":"crossref","unstructured":"Aspinall, D.: Proof General: a generic tool for proof development. In: TACAS, vol. 1785 LNCS, pp. 38\u201342. Springer, (2000)","DOI":"10.1007\/3-540-46419-0_3"},{"key":"457_CR2","doi-asserted-by":"crossref","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. In: Calculemus\/MKM, pp. 161\u2013175, (2007)","DOI":"10.1007\/978-3-540-73086-6_15"},{"key":"457_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec $$^\\sharp $$ \u266f programming system: an overview. In: CASSIS, pp. 49\u201369, (2005)","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"457_CR4","doi-asserted-by":"crossref","unstructured":"Barras, B., Tankink, C., Tassi, E.: Asynchronous processing of Coq documents: from the kernel up to the user interface. In: Proceedings of ITP, Nanjing, China, (August 2015)","DOI":"10.1007\/978-3-319-22102-1_4"},{"key":"457_CR5","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/978-3-642-22863-6_5","volume":"6898","author":"Jesper Bengtson","year":"2011","unstructured":"Bengtson, Jesper: Jensen, Jonas Braband, Sieczkowski, Filip, Birkedal, Lars: Verifying object-oriented programs with higher-order separation logic in Coq. Lect Notes Comput Sci 6898, 22\u201338 (2011)","journal-title":"Lect Notes Comput Sci"},{"key":"457_CR6","doi-asserted-by":"crossref","unstructured":"Boldo, S., Jourdan, J-H., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: ARITH, pp. 107\u2013115. IEEE Computer Society, (2013)","DOI":"10.1109\/ARITH.2013.30"},{"key":"457_CR7","unstructured":"Bros, N., Cerioli, R.: OcaIDE. Software, http:\/\/www.algo-prog.info\/ocaide\/"},{"key":"457_CR8","unstructured":"Charles, J., Kiniry, J.R.: A lightweight theorem prover interface for Eclipse. In: UITP Workshop proceedings, (2008)"},{"key":"457_CR9","unstructured":"Eclipse Foundation. EGit. Software, http:\/\/www.eclipse.org\/egit\/"},{"key":"457_CR10","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns\u2014Elements of Reusable Object-Oriented Software. Addison\u2013Wesley, (1994). First edition, 20th printing"},{"key":"457_CR11","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: ITP, pp. 163\u2013179. Springer, (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"457_CR12","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)"},{"key":"457_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139193894","volume-title":"Dense Sphere Packings \u2013A Blueprint for Formal Proofs","author":"Thomas C Hales","year":"2012","unstructured":"Hales, Thomas C.: Dense Sphere Packings \u2013A Blueprint for Formal Proofs. Cambridge University Press, Cambridge (2012)"},{"key":"457_CR14","unstructured":"Harrison, J.: HOL Light: an overview. In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 60\u201366, (2009)"},{"key":"457_CR15","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. CW Reports CW520, Department of Computer Science, K.U.Leuven, (August 2008)"},{"issue":"1","key":"457_CR16","first-page":"2","volume":"32","author":"Gerwin Klein","year":"2014","unstructured":"Klein, Gerwin, Andronick, June, Elphinstone, Kevin, Murray, Toby C., Sewell, Thomas, Kolanski, Rafal, Heiser, Gernot: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"457_CR17","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR-16, pp. 348\u2013370, (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"457_CR18","doi-asserted-by":"crossref","unstructured":"Magnusson, L., Nordstr\u00f6m, B.: The ALF proof editor and its proof engine. In: Types for proofs and programs, pp. 213\u2013237. Springer, (1994)","DOI":"10.1007\/3-540-58085-9_78"},{"key":"457_CR19","unstructured":"Mehnert, H.: Kopitiam: modular incremental interactive full functional static verification of Java code. In: NASA Formal Methods\u2014Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18\u201320, 2011. Proceedings, pp. 518\u2013524, (2011)"},{"key":"457_CR20","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden, (September 2007)"},{"key":"457_CR21","doi-asserted-by":"crossref","unstructured":"Ring, M., L\u00fcth, C.: Collaborative interactive theorem proving with Clide. In: ITP, pp. 467\u2013482. Springer, (2014)","DOI":"10.1007\/978-3-319-08970-6_30"},{"key":"457_CR22","unstructured":"The Coq Development Team. The Coq reference manual. http:\/\/coq.inria.fr\/doc"},{"key":"457_CR23","unstructured":"Velykis, A.: Isabelle\/Eclipse. Software, http:\/\/andriusvelykis.github.io\/isabelle-eclipse"},{"key":"457_CR24","unstructured":"Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle\/PIDE. In: ITP, vol. 8558 of LNCS, pp. 515\u2013530. Springer, (2014)"},{"key":"457_CR25","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: System description: Isabelle\/jEdit in 2014. In: UITP, (2014)","DOI":"10.4204\/EPTCS.167.10"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0457-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0457-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0457-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T14:59:28Z","timestamp":1569164368000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0457-2"}},"subtitle":["An IDE for interactive proof development in Coq"],"short-title":[],"issued":{"date-parts":[[2017,5,2]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["457"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0457-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,2]]}}}