{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:53:03Z","timestamp":1740099183581,"version":"3.37.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030027674"},{"type":"electronic","value":"9783030027681"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-02768-1_9","type":"book-chapter","created":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:42:27Z","timestamp":1540107747000},"page":"157-165","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General"],"prefix":"10.1007","author":[{"given":"Hideyuki","family":"Kawabata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuta","family":"Tanaka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mai","family":"Kimura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tetsuo","family":"Hironaka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"9_CR1","unstructured":"The compcert project. \nhttp:\/\/compcert.inria.fr"},{"key":"9_CR2","unstructured":"Lablgtk2. \nhttp:\/\/lablgtk.forge.ocamlcore.org"},{"key":"9_CR3","unstructured":"Pcoq: a graphical user-interface for coq. \nhttp:\/\/www-sop.inria.fr\/lemme\/pcoq\/"},{"key":"9_CR4","unstructured":"The sel4 microkernel. \nhttp:\/\/sel4.systems"},{"issue":"2","key":"9_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. J. Autom. Reason. 39(2), 109\u2013139 (2007)","journal-title":"J. Autom. Reason."},{"key":"9_CR6","unstructured":"Bedford, A.: Coqatoo: generating natural language versions of coq proofs. In: 4th International Workshop on Coq for Programming Languages (2018)"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.entcs.2008.12.095","volume":"226","author":"J Byrnes","year":"2009","unstructured":"Byrnes, J., Buchanan, M., Ernst, M., Miller, P., Roberts, C., Keller, R.: Visualizing proof search for theorem prover development. Electron. Notes Theor. Comput. Sci. 226, 23\u201338 (2009)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative language for the coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 69\u201384. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-68103-8_5"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/BFb0014048","volume-title":"Typed Lambda Calculi and Applications","author":"Y Coscoy","year":"1995","unstructured":"Coscoy, Y., Kahn, G., Th\u00e9ry, L.: Extracting text from proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 109\u2013123. Springer, Heidelberg (1995). \nhttps:\/\/doi.org\/10.1007\/BFb0014048"},{"issue":"2","key":"9_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1093\/comjnl\/38.2.91","volume":"38","author":"P Curzon","year":"1995","unstructured":"Curzon, P.: Tracking design changes with formal machine-checked proof. Comput. J. 38(2), 91\u2013100 (1995). \nhttps:\/\/doi.org\/10.1093\/comjnl\/38.2.91","journal-title":"Comput. J."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.118.1","volume":"118","author":"Cvetan Dunchev","year":"2013","unstructured":"Dunchev, C., et al.: Prooftool: a GUI for the GAPT framework. In: Proceedings 10th International Workshop On User Interfaces for Theorem Provers (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/3-540-45744-5_33","volume-title":"Automated Reasoning","author":"A Fiedler","year":"2001","unstructured":"Fiedler, A.: P.rex: an interactive proof explainer. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 416\u2013420. Springer, Heidelberg (2001). \nhttps:\/\/doi.org\/10.1007\/3-540-45744-5_33"},{"key":"9_CR13","unstructured":"Giero, M., Wiedijk, F.: MMode, a Mizar Mode for the proof assistant coq. Technical report, Nijmegen Institute for Computing and Information Sciences (2003)"},{"key":"9_CR14","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem (2006). \nhttp:\/\/www2.tcs.ifi.lmu.de\/~abel\/lehre\/WS07-08\/CAFR\/4colproof.pdf"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"issue":"2","key":"9_CR16","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in coq. J. Form. Reason. 3(2), 95\u2013152 (2010)","journal-title":"J. Form. Reason."},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: A mizar mode for HOL. In: Goos, G., Hartmanis, J., van Leeuwen, J., von Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 203\u2013220. Springer, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/BFb0105406"},{"key":"9_CR18","first-page":"35","volume":"3","author":"M Hendriks","year":"2010","unstructured":"Hendriks, M., Kaliszyk, C., van Raamsdonk, F., Wiedijk, F.: Teaching logic using a state-of-the-art proof assistant. Acta Didact. Napoc. 3, 35\u201348 (2010)","journal-title":"Acta Didact. Napoc."},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"35","DOI":"10.4204\/EPTCS.167.6","volume":"167","author":"Tomer Libal","year":"2014","unstructured":"Libal, T., Riener, M., Rukhaia, M.: Advanced proof viewing in ProofTool. In: Eleventh Workshop on User Interfaces for Theorem Provers (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-20551-4_6","volume-title":"Logic-Based Program Synthesis and Transformation","author":"K Sakurai","year":"2011","unstructured":"Sakurai, K., Asai, K.: MikiBeta : a general GUI library for visualizing proof trees. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol. 6564, pp. 84\u201398. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-20551-4_6"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-14128-7_37","volume-title":"Intelligent Computer Mathematics","author":"C Tankink","year":"2010","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: a tool for proof re-animation. In: Autexier, S., et al. (eds.) CICM 2010. LNCS (LNAI), vol. 6167, pp. 440\u2013454. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-14128-7_37"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-17796-5_10","volume-title":"Algebraic Methodology and Software Technology","author":"J Tesson","year":"2011","unstructured":"Tesson, J., Hashimoto, H., Hu, Z., Loulergue, F., Takeichi, M.: Program calculation in coq. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 163\u2013179. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17796-5_10"},{"key":"9_CR23","unstructured":"Tews, H.: Prooftree. \nhttps:\/\/askra.de\/software\/prooftree\/"},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.entcs.2006.09.025","volume":"174","author":"S Trac","year":"2007","unstructured":"Trac, S., Puzis, Y., Sutcliffe, G.: An interactive derivation viewer. Electron. Notes Theor. Comput. Sci. 174(2), 109\u2013123 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1023\/A:1021935419355","volume":"29","author":"M Wenzel","year":"2002","unstructured":"Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29, 389\u2013411 (2002)","journal-title":"J. Autom. Reason."},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/11542384","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11542384"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02768-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,10,21]],"date-time":"2018-10-21T07:45:47Z","timestamp":1540107947000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-02768-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030027674","9783030027681"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-02768-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Wellington","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/aplas2018.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}