{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T07:04:01Z","timestamp":1725865441892},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_19","type":"book-chapter","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:11:57Z","timestamp":1474409517000},"page":"333-348","source":"Crossref","is-referenced-by-count":1,"title":["ProofScript: Proof Scripting for the Masses"],"prefix":"10.1007","author":[{"given":"Steven","family":"Obua","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Phil","family":"Scott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"19_CR1","unstructured":"ProofPeer. http:\/\/www.proofpeer.net"},{"key":"19_CR2","unstructured":"Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: ProofPeer: Collaborative Theorem Proving. arXiv: 1404.6186 (2013)"},{"key":"19_CR3","unstructured":"ProofScript. http:\/\/proofpeer.net\/topics\/proofscript"},{"key":"19_CR4","unstructured":"Obua, S., Scott, P., Fleuriot, J.: Local Lexing. http:\/\/proofpeer.net\/papers\/locallexing"},{"key":"19_CR5","unstructured":"Scott, P., Obua, S., Fleuriot, J.: Bootstrapping LCF Declarative Proofs. http:\/\/proofpeer.net\/papers\/bootstrapping"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48256-3_12"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-60275-5_55","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"S Agerholm","year":"1995","unstructured":"Agerholm, S., Gordon, M.: Experiments with ZF set theory in HOL and Isabelle. In: Thomas Schubert, E., Windley, P.J., Alves-Foss, J. (eds.) TPHOLs 1995. LNCS, vol. 971, pp. 32\u201345. Springer, Heidelberg (1995). doi: 10.1007\/3-540-60275-5_55"},{"key":"19_CR8","unstructured":"ProofPeer Root Theory. http:\/\/proofpeer.net\/repository?root.thy"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-319-08970-6_25","volume-title":"Interactive Theorem Proving","author":"D Matichuk","year":"2014","unstructured":"Matichuk, D., Wenzel, M., Murray, T.: An Isabelle proof method language. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 390\u2013405. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-08970-6_25"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M Gordon","year":"1979","unstructured":"Gordon, M., Milner, A., Wadsworth, C.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979). doi: 10.1007\/3-540-09724-4"},{"key":"19_CR11","unstructured":"Obua, S.: Purely Functional Structured Programming. arXiv:1007.3023 (2010)"},{"key":"19_CR12","unstructured":"Okasaki, C.: In praise of mandatory indentation for novice programmers, February 2008. http:\/\/okasaki.blogspot.co.uk\/2008\/02\/in-praise-of-mandatory-indentation-for.html"},{"key":"19_CR13","doi-asserted-by":"publisher","unstructured":"Landin, P.: The Next 700 Programming Languages (1966). doi: 10.1145\/365230.365257","DOI":"10.1145\/365230.365257"},{"issue":"3","key":"19_CR14","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L Paulson","year":"1993","unstructured":"Paulson, L.: Set theory for verification: I. From foundations to functions. J. Autom. Reason. 11(3), 353\u2013389 (1993). doi: 10.1007\/BF00881873","journal-title":"J. Autom. Reason."},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BF00881916","volume":"15","author":"L Paulson","year":"1995","unstructured":"Paulson, L.: Set theory for verification: II. Induction and recursion. J. Autom. Reason. 15, 167\u2013215 (1995). doi: 10.1007\/BF00881916","journal-title":"J. Autom. Reason."},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11921240_19","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"S Obua","year":"2006","unstructured":"Obua, S.: Partizan games in Isabelle\/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 272\u2013286. Springer, Heidelberg (2006). doi: 10.1007\/11921240_19"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-20615-8_6","volume-title":"Intelligent Computer Mathematics","author":"S Obua","year":"2015","unstructured":"Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: Type inference for ZFH. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 87\u2013101. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-20615-8_6"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0038698","volume-title":"Extensions of Logic Programming","author":"D Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS, vol. 475, pp. 253\u2013281. Springer, Heidelberg (1991). doi: 10.1007\/BFb0038698"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Functional Unification of Higher-Order Patterns (1993). doi: 10.1109\/LICS.1993.287599","DOI":"10.1109\/LICS.1993.287599"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T22:18:38Z","timestamp":1474409918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}