{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T19:02:39Z","timestamp":1776884559188,"version":"3.51.2"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319948201","type":"print"},{"value":"9783319948218","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94821-8_25","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"432-440","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Towards Verified Handwritten Calculational Proofs"],"prefix":"10.1007","author":[{"given":"Alexandra","family":"Mendes","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"25_CR1","unstructured":"Anderson, R., Anderson, R., Chung, O., Davis, K.M., Davis, P., Prince, C., Razmov, V., Simon, B.: Classroom presenter - a classroom interaction system for active and collaborative learning. In: WIPTE (2006)"},{"key":"25_CR2","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). \n                    https:\/\/doi.org\/10.1007\/3-540-46419-0_3"},{"issue":"3","key":"25_CR3","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(94)00212-H","volume":"53","author":"R Backhouse","year":"1995","unstructured":"Backhouse, R.: The calculational method. Inf. Process. Lett. 53(3), 121 (1995)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"25_CR4","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/j.scico.2010.05.006","volume":"76","author":"R Backhouse","year":"2011","unstructured":"Backhouse, R., Ferreira, J.F.: On Euclid\u2019s algorithm and elementary number theory. Sci. Comput. Program. 76(3), 160\u2013180 (2011). \n                    https:\/\/doi.org\/10.1016\/j.scico.2010.05.006\n                    \n                  . \n                    http:\/\/joaoff.com\/publications\/2010\/euclid-alg","journal-title":"Sci. Comput. Program."},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11783596_7","volume-title":"Mathematics of Program Construction","author":"R Backhouse","year":"2006","unstructured":"Backhouse, R., Michaelis, D.: Exercises in quantifier manipulation. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 69\u201381. Springer, Heidelberg (2006). \n                    https:\/\/doi.org\/10.1007\/11783596_7"},{"key":"25_CR6","unstructured":"Backhouse, R., Verhoeven, R.: \n                    \n                      \n                    \n                    $${\\sf Math }\\!\\!\\int \\!\\!{\\sf pad}$$\n                  : a system for on-line preparation of mathematical documents. Softw. Concepts Tools 18, 80\u201389 (1997)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-44755-5_7","volume-title":"Theorem Proving in Higher Order Logics","author":"G Bauer","year":"2001","unstructured":"Bauer, G., Wenzel, M.: Calculational reasoning revisited an Isabelle\/Isar experience. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75\u201390. Springer, Heidelberg (2001). \n                    https:\/\/doi.org\/10.1007\/3-540-44755-5_7"},{"key":"25_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"25_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"EW Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, New York (1990). \n                    https:\/\/doi.org\/10.1007\/978-1-4612-3228-5"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Ferreira, J.F., Mendes, A.: Students\u2019 feedback on teaching mathematics through the calculational method. In: 39th ASEE\/IEEE Frontiers in Education Conference. IEEE (2009)","DOI":"10.1109\/FIE.2009.5350478"},{"issue":"5, Part 2","key":"25_CR11","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1016\/j.jlamp.2015.11.004","volume":"85","author":"JF Ferreira","year":"2016","unstructured":"Ferreira, J.F., Mendes, A.: A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebra. J. Log. Algebraic Methods Program. 85(5, Part 2), 906\u2013920 (2016). \n                    https:\/\/doi.org\/10.1016\/j.jlamp.2015.11.004\n                    \n                  . \n                    http:\/\/www.sciencedirect.com\/science\/article\/pii\/S2352220815001418\n                    \n                  . Articles dedicated to Prof. J. N. Oliveira on the occasion of his 60th birthday","journal-title":"J. Log. Algebraic Methods Program."},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-04912-5_4","volume-title":"Teaching Formal Methods","author":"JF Ferreira","year":"2009","unstructured":"Ferreira, J.F., Mendes, A., Backhouse, R., Barbosa, L.S.: Which mathematics for the information society? In: Gibbons, J., Oliveira, J.N. (eds.) TFM 2009. LNCS, vol. 5846, pp. 39\u201356. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-04912-5_4"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-642-21350-2_8","volume-title":"Tools for Teaching Logic","author":"JF Ferreira","year":"2011","unstructured":"Ferreira, J.F., Mendes, A., Cunha, A., Baquero, C., Silva, P., Barbosa, L.S., Oliveira, J.N.: Logic training through algorithmic problem solving. In: Blackburn, P., van Ditmarsch, H., Manzano, M., Soler-Toscano, F. (eds.) TICTTL 2011. LNCS (LNAI), vol. 6680, pp. 62\u201369. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-21350-2_8"},{"key":"25_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A Logical Approach to Discrete Math","author":"D Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Springer, New York (1993)"},{"issue":"8","key":"25_CR15","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1080\/00029890.1995.12004644","volume":"102","author":"D Gries","year":"1995","unstructured":"Gries, D., Schneider, F.B.: Teaching math more effectively, through calculational proofs. Am. Math. Mon. 102(8), 691\u2013697 (1995)","journal-title":"Am. Math. Mon."},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24452-0_1","volume-title":"Implementation and Application of Functional Languages","author":"R Hinze","year":"2011","unstructured":"Hinze, R.: Scans and convolutions\u2014a calculational proof of Moessner\u2019s theorem. In: Scholz, S.-B., Chitil, O. (eds.) IFL 2008. LNCS, vol. 5836, pp. 1\u201324. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-24452-0_1"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-24771-5_16","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 178\u2013190. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-24771-5_16"},{"key":"25_CR18","doi-asserted-by":"publisher","unstructured":"Labahn, G., Lank, E., MacLean, S., Marzouk, M., Tausky, D.: Mathbrush: a system for doing math on pen-based devices. In: Proceedings of the 2008 The Eighth IAPR International Workshop on Document Analysis Systems, DAS 2008, pp. 599\u2013606. IEEE Computer Society, Washington, DC (2008). \n                    https:\/\/doi.org\/10.1109\/DAS.2008.21","DOI":"10.1109\/DAS.2008.21"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-642-54108-7_9","volume-title":"Verified Software: Theories, Tools, Experiments","author":"KRM Leino","year":"2014","unstructured":"Leino, K.R.M., Polikarpova, N.: Verified calculations. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 170\u2013190. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-642-54108-7_9"},{"key":"25_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-39320-4_22","volume-title":"Intelligent Computer Mathematics","author":"C L\u00fcth","year":"2013","unstructured":"L\u00fcth, C., Ring, M.: A web interface for Isabelle: the next generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 326\u2013329. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39320-4_22"},{"issue":"2\u20134","key":"25_CR22","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0020-0190(00)00200-3","volume":"77","author":"P Manolios","year":"2001","unstructured":"Manolios, P., Moore, J.S.: On the desirability of mechanizing calculational proofs. Inf. Process. Lett. 77(2\u20134), 173\u2013179 (2001). \n                    https:\/\/doi.org\/10.1016\/S0020-0190(00)00200-3","journal-title":"Inf. Process. Lett."},{"key":"25_CR23","unstructured":"Mendes, A.: Structured editing of handwritten mathematics. Ph.D. thesis, School of Computer Science, University of Nottingham (2012)"},{"key":"25_CR24","doi-asserted-by":"publisher","unstructured":"Mendes, A., Backhouse, R., Ferreira, J.F.: Structure editing of handwritten mathematics: improving the computer support for the calculational method. In: Proceedings of the Ninth ACM International Conference on Interactive Tabletops and Surfaces, ITS 2014, pp. 139\u2013148. ACM, New York (2014). \n                    https:\/\/doi.org\/10.1145\/2669485.2669495","DOI":"10.1145\/2669485.2669495"},{"key":"25_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2016","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2016). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9\n                    \n                  . \n                    https:\/\/isabelle.in.tum.de\/doc\/prog-prove.pdf"},{"key":"25_CR26","unstructured":"Microsoft OneNote. \n                    https:\/\/www.onenote.com\n                    \n                  . Accessed 02 Feb 2018"},{"key":"25_CR27","unstructured":"Pit-Claudel, C., Courtieu, P.: Company-Coq: taking proof general one step closer to a real IDE. In: CoqPL 2016: International Workshop on Coq for Programming Languages (2016)"},{"key":"25_CR28","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). \n                    https:\/\/doi.org\/10.1007\/978-3-642-17796-5_10"},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF02298246","volume":"38","author":"SD Tripp","year":"1990","unstructured":"Tripp, S.D., Bichelmeyer, B.: Rapid prototyping: an alternative instructional design strategy. Educ. Tech. Res. Dev. 38(1), 31\u201344 (1990)","journal-title":"Educ. Tech. Res. Dev."},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1128","DOI":"10.1007\/3-540-48118-4_10","volume-title":"FM 1999 \u2014 Formal Methods","author":"R Verhoeven","year":"1999","unstructured":"Verhoeven, R., Backhouse, R.: Interfacing program construction and verification. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1128\u20131146. Springer, Heidelberg (1999). \n                    https:\/\/doi.org\/10.1007\/3-540-48118-4_10\n                    \n                  . \n                    http:\/\/dl.acm.org\/citation.cfm?id=647545.730778"},{"key":"25_CR31","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., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 468\u2013471. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-31374-5_38"},{"key":"25_CR32","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). \n                    https:\/\/doi.org\/10.1007\/978-3-319-08970-6_33"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Wolff, B.: Isabelle\/PIDE as platform for educational tools. arXiv preprint \n                    arXiv:1202.4835\n                    \n                   (2012)","DOI":"10.4204\/EPTCS.79.9"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T13:42:22Z","timestamp":1578490942000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_25"}},"subtitle":["(Short Paper)"],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"4 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","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":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}