{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:55:29Z","timestamp":1776552929991,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642226724","type":"print"},{"value":"9783642226731","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_18","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T11:49:15Z","timestamp":1310557755000},"page":"260-275","source":"Crossref","is-referenced-by-count":11,"title":["Towards Formal Proof Script Refactoring"],"prefix":"10.1007","author":[{"given":"Iain","family":"Whiteside","sequence":"first","affiliation":[]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[]},{"given":"Lucas","family":"Dixon","sequence":"additional","affiliation":[]},{"given":"Gudmund","family":"Grov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s11786-010-0025-6","volume":"3","author":"D. Aspinall","year":"2010","unstructured":"Aspinall, D., Denney, E., L\u00fcth, C.: Tactics for hierarchical proof. Mathematics in Computer Science\u00a03, 309\u2013330 (2010)","journal-title":"Mathematics in Computer Science"},{"key":"18_CR2","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.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"issue":"3","key":"18_CR3","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S1571-0661(05)82564-2","volume":"70","author":"M. Cornlio","year":"2002","unstructured":"Cornlio, M., Cavalcanti, A., Sampaio, A.: Refactoring by transformation. Electronic Notes in Theoretical Computer Science\u00a070(3), 311\u2013330 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.entcs.2005.11.063","volume":"155","author":"E. Denney","year":"2006","unstructured":"Denney, E., Power, J., Tourlas, K.: Hiproofs: A hierarchical notion of proof tree. Electr. Notes Theor. Comput. Sci.\u00a0155, 341\u2013359 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR5","unstructured":"Ettinger, R., Verbaere, M.: Refactoring bugs in Eclipse, IntelliJ IDEA and Visual Studio (2005), http:\/\/progtools.comlab.ox.ac.uk\/projects\/refactoring\/bugreports"},{"key":"18_CR6","volume-title":"Refactoring: improving the design of existing code","author":"M. Fowler","year":"1999","unstructured":"Fowler, M.: Refactoring: improving the design of existing code. Addison-Wesley, Reading (1999)"},{"key":"18_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: The Four Colour Theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol.\u00a05081, pp. 333\u2013333. Springer, Heidelberg (2008)"},{"key":"18_CR8","first-page":"1370","volume":"55","author":"T.C. Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Notices of the AMS\u00a055, 1370\u20131380 (2008)","journal-title":"Notices of the AMS"},{"key":"18_CR9","first-page":"207","volume-title":"Proceedings of the 22nd ACM Symposium on OSP","author":"G. Klein","year":"2009","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on OSP, pp. 207\u2013220. ACM, New York (October 2009)"},{"key":"18_CR10","unstructured":"Li, H., Thompson, S.: Formalisation of Haskell Refactorings. In: Trends in Functional Programming (September 2005)"},{"issue":"2","key":"18_CR11","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1109\/TSE.2004.1265817","volume":"30","author":"T. Mens","year":"2004","unstructured":"Mens, T., Tourwe, T.: A survey of software refactoring. IEEE Trans. Softw. Eng.\u00a030(2), 126\u2013139 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"18_CR12","unstructured":"Opdyke, W.F.: Refactoring object-oriented frameworks. PhD thesis, University of Illinois, Champaign, IL, USA (1992)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Pons, O., Bertot, Y., Rideau, L.: Notions of dependency in proof assistants. In: User Interfaces for Theorem Provers, UITP (1998)","DOI":"10.1006\/jsco.1997.0171"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-45719-4_30","volume-title":"Algebraic Methodology and Software Technology","author":"A. Schairer","year":"2002","unstructured":"Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 441\u2013456. Springer, Heidelberg (2002)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/3-540-45500-0_27","volume-title":"Theoretical Aspects of Computer Software","author":"A. Serjantov","year":"2001","unstructured":"Serjantov, A., Sewell, P., Wansbrough, K.: The UDP calculus: Rigorous semantics for real networking. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 535\u2013559. Springer, Heidelberg (2001)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Stepney, S., Polack, F., Toyn, I.: Refactoring in maintenance and development of Z specifications. Electr. Notes Theor. Comput. Sci. 70(3) (2002)","DOI":"10.1016\/S1571-0661(05)80485-2"},{"issue":"2","key":"18_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.entcs.2006.09.022","volume":"174","author":"U. Josef","year":"2007","unstructured":"Josef, U., Grzegorz, B.: Presenting and explaining Mizar. Electron. Notes Theor. Comput. Sci.\u00a0174(2), 63\u201374 (2007)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR18","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 - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 167\u2013184. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:34Z","timestamp":1560381574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}