{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:20Z","timestamp":1726034660919},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_1","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"1-15","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Interaction with Formal Mathematical Documents in Isabelle\/PIDE"],"prefix":"10.1007","author":[{"given":"Makarius","family":"Wenzel","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: a generic tool for proof development. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 38\u201343. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46419-0_3"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-73086-6_15","volume-title":"Towards Mechanized Mathematical Assistants","author":"D Aspinall","year":"2007","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM 2007. LNCS (LNAI), vol. 4573, pp. 161\u2013175. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_15"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-39320-4_29","volume-title":"Intelligent Computer Mathematics","author":"B Barras","year":"2013","unstructured":"Barras, B., et al.: Pervasive parallelism in highly-trustable interactive theorem proving systems. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 359\u2013363. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39320-4_29"},{"key":"1_CR4","unstructured":"Bertot, Y., Th\u00e9ry, L.: A generic approach to building user interfaces for theorem provers. J. Symbolic Comput. 11 (1996)"},{"key":"1_CR5","unstructured":"Blanchette, J.C.: Hammering away: a user\u2019s guide to Sledgehammer for Isabelle\/HOL. Isabelle Documentation (2019)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Condoluci, A., Kohlhase, M., M\u00fcller, D., Rabe, F., Sacerdoti Coen, C., Wenzel, M.: Relational data across mathematical libraries. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) Intelligent Computer Mathematics, CICM 2019, LNAI 11617, pp. 61\u201376. Springer, Heidelberg (2019)","DOI":"10.1007\/978-3-030-23250-4_5"},{"key":"1_CR7","unstructured":"Eberl, M., Klein, G., Nipkow, T., Paulson, L., Thiemann, R. (eds.): The Archive of Formal Proofs (AFP). https:\/\/dblp.uni-trier.de\/db\/journals\/afp"},{"key":"1_CR8","unstructured":"Frerix, S., Koepke, P.: Automatic proof-checking of ordinary mathematical texts. In: Workshop on Formal Mathematics for Mathematicians (FMM 2018). CICM Informal Proceedings (2018). https:\/\/www.cicm-conference.org\/2018\/infproc\/paper13.pdf"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Morris, L., Newey, M.C., Wadsworth, C.P.: A metalanguage for interactive proof in LCF. In: Principles of programming languages (POPL) (1978)","DOI":"10.1145\/512760.512773"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF. A Mechanised Logic of Computation","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09724-4"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-27818-4_17","volume-title":"Mathematical Knowledge Management","author":"A Lyaletski","year":"2004","unstructured":"Lyaletski, A., Paskevich, A., Verchinine, K.: Theorem proving and proof verification in the system SAD. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 236\u2013250. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27818-4_17"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Matthews, D., Wenzel, M.: Efficient parallel programming in Poly\/ML and Isabelle\/ML. In: ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010) (2010)","DOI":"10.1145\/1708046.1708058"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Pretty printing. ACM Trans. Program. Lang. Syst. 2(4) (1980)","DOI":"10.1145\/357114.357115"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.4204\/EPTCS.167.9","volume":"167","author":"Carst Tankink","year":"2014","unstructured":"Tankink, C.: PIDE for asynchronous interaction with Coq. In: Benzm\u00fcller, C., Woltzenlogel Paleo, B. (eds.) User Interfaces for Theorem Provers (UITP 2014), EPTCS, vol. 167 (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.9","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1_CR15","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Dos Reis, G., Th\u00e9ry, L. (eds.) ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library (2009)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 244\u2013259. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_17"},{"key":"1_CR17","unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 a generic framework for human-readable proof documents. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof \u2013 Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, vol. 10, no. 23. University of Bia\u0142ystok (2007)"},{"key":"1_CR18","unstructured":"Wenzel, M.: On prover interaction and integration with Isabelle\/Scala. In: Ball, T., Giesl, J., H\u00e4hnle, R., Nipkow, T. (eds.) Interaction versus Automation: the Two Faces of Deduction (Dagstuhl Seminar 09411). Schloss Dagstuhl, Germany, October 2009. http:\/\/drops.dagstuhl.de\/portals\/09411 , https:\/\/files.sketis.net\/Dagstuhl2009.pdf"},{"key":"1_CR19","unstructured":"Wenzel, M.: Asynchronous proof processing with Isabelle\/Scala and Isabelle\/jEdit. In: Coen, C.S., Aspinall, D. (eds.) User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop. ENTCS, Elsevier, July 2010"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2012","unstructured":"Wenzel, M.: Isabelle\/jEdit \u2013 a prover IDE within the PIDE framework. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 468\u2013471. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_38 . https:\/\/arxiv.org\/abs\/1207.3441"},{"key":"1_CR21","unstructured":"Wenzel, M.: PIDE as front-end technology for Coq (2013). https:\/\/arxiv.org\/abs\/1304.6626"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"57","DOI":"10.4204\/EPTCS.118.4","volume":"118","author":"Makarius Wenzel","year":"2013","unstructured":"Wenzel, M.: READ-EVAL-PRINT in parallel and asynchronous proof-checking. In: Kaliszyk, C., L\u00fcth, C. (eds.) User Interfaces for Theorem Provers UITP 2012, EPTCS, vol. 118 (2013). https:\/\/doi.org\/10.4204\/EPTCS.118.4","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-39634-2_30","volume-title":"Interactive Theorem Proving","author":"M Wenzel","year":"2013","unstructured":"Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 418\u2013434. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_30"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-319-08970-6_33","volume-title":"Interactive Theorem Proving","author":"M Wenzel","year":"2014","unstructured":"Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle\/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515\u2013530. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_33"},{"key":"1_CR25","unstructured":"Wenzel, M.: System description: Isabelle\/jEdit in 2014. In: Benzm\u00fcller, C., Woltzenlogel Paleo, B. (eds.) User Interfaces for Theorem Provers, UITP 2014, EPTCS, July 2014. http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?UITP2014:11"},{"key":"1_CR26","unstructured":"Wenzel, M.: Further scaling of Isabelle technology. In: Isabelle Workshop 2018, Oxford, UK (2018). https:\/\/files.sketis.net\/Isabelle_Workshop_2018\/Isabelle_2018_paper_1.pdf"},{"key":"1_CR27","unstructured":"Wenzel, M.: The Isabelle prover IDE after 10 years of development. In: Bauer, A., Escard\u00f3, M., Lumsdaine, P.L., Mahboubi, A. (eds.) Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Schloss Dagstuhl, Germany, August 2018. https:\/\/www.dagstuhl.de\/18341 , https:\/\/sketis.net\/2018\/the-isabelle-prover-ide-after-10-years-of-development"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"71","DOI":"10.4204\/EPTCS.284.6","volume":"284","author":"Makarius Wenzel","year":"2018","unstructured":"Wenzel, M.: Isabelle\/jEdit as IDE for domain-specific formal languages and informal text documents. In: Masci, P., Monahan, R., Prevosto, V. (eds.) F-IDE Workshop 2018, Oxford, UK, no. 284. EPTCS (2018). http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FIDE2018.6","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1_CR29","unstructured":"Wenzel, M.: Isabelle\/PIDE after 10 years of development. In: User Interfaces for Theorem Provers, UITP 2018 (2018). https:\/\/sketis.net\/wp-content\/uploads\/2018\/08\/isabelle-pide-uitp2018.pdf"},{"key":"1_CR30","unstructured":"Wenzel, M.: Isabelle\/jEdit. Isabelle Documentation (2019)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T20:21:43Z","timestamp":1575231703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}