{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:35Z","timestamp":1774837955724,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642452208","type":"print"},{"value":"9783642452215","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_52","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"776-791","source":"Crossref","is-referenced-by-count":5,"title":["Polar: A Framework for Proof Refactoring"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Dietrich","sequence":"first","affiliation":[]},{"given":"Iain","family":"Whiteside","sequence":"additional","affiliation":[]},{"given":"David","family":"Aspinall","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"52_CR1","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/s10664-011-9158-8","volume":"16","author":"T.B.C. Arias","year":"2011","unstructured":"Arias, T.B.C., van der Spek, P., Avgeriou, P.: A practice-driven systematic review of dependency analysis solutions. Empirical Software Engineering\u00a016(5), 544\u2013586 (2011)","journal-title":"Empirical Software Engineering"},{"key":"52_CR2","doi-asserted-by":"publisher","first-page":"2401","DOI":"10.1098\/rsta.2005.1655","volume":"363","author":"M. Aschbacher","year":"2005","unstructured":"Aschbacher, M.: Highly complex proofs and implications of such proofs. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences\u00a0363, 2401\u20132406 (2005)","journal-title":"Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences"},{"key":"52_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-34026-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"S. Autexier","year":"2012","unstructured":"Autexier, S., Dietrich, D., Hutter, D., L\u00fcth, C., Maeder, C.: Smartties - management of safety-critical developments. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 238\u2013252. Springer, Heidelberg (2012)"},{"issue":"4","key":"52_CR4","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1145\/319628.319634","volume":"6","author":"F. Bancilhon","year":"1981","unstructured":"Bancilhon, F., Spyratos, N.: Update semantics of relational views. ACM Trans. Database Syst.\u00a06(4), 557\u2013575 (1981)","journal-title":"ACM Trans. Database Syst."},{"key":"52_CR5","unstructured":"Bell Canada. DATRIX abstract semantic graph reference manual (version 1.4). Technical report (2000)"},{"key":"52_CR6","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-31374-5_3","volume-title":"Intelligent Computer Mathematics","author":"T. Bourke","year":"2012","unstructured":"Bourke, T., Daum, M., Klein, G., Kolanski, R.: Challenges and experiences in managing large-scale proofs. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 32\u201348. Springer, Heidelberg (2012)"},{"key":"52_CR7","doi-asserted-by":"crossref","unstructured":"Chen, H., Liao, H.: A comparative study of view update problem. In: Data Storage and Data Engineering (DSDE), pp. 83\u201389 (2010)","DOI":"10.1109\/DSDE.2010.42"},{"issue":"3","key":"52_CR8","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2007.02.001","volume":"376","author":"J. Lara de","year":"2007","unstructured":"de Lara, J., Bardohl, R., Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Attributed graph transformation with node type inheritance. Theor. Comput. Sci.\u00a0376(3), 139\u2013163 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"52_CR9","unstructured":"Dietrich, D.: Assertion Level Proof Planning with Compiled Strategies. PhD thesis, Saarland University (2011)"},{"issue":"3","key":"52_CR10","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J. Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst.\u00a09(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"52_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/11841883_27","volume-title":"Graph Transformations","author":"R. Gei\u00df","year":"2006","unstructured":"Gei\u00df, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: A fast SPO-based graph rewriting tool. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol.\u00a04178, pp. 383\u2013397. Springer, Heidelberg (2006)"},{"key":"52_CR12","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, p. 333. Springer, Heidelberg (2008)"},{"key":"52_CR13","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.\u00a07998, pp. 163\u2013179. Springer, Heidelberg (2013)"},{"key":"52_CR14","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. Rapport de recherche RR-6156, INRIA (2007)"},{"key":"52_CR15","first-page":"119","volume-title":"Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978","author":"M. Gordon","year":"1978","unstructured":"Gordon, M., Milner, R., Morris, L., Newey, M., Wadsworth, C.: A metalanguage for interactive proof in LCF. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1978, pp. 119\u2013130. ACM, New York (1978)"},{"key":"52_CR16","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol.\u00a005021 (2006)"},{"key":"52_CR17","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Pierce, B., Wagner, D.: Edit lenses. In: ACM SIGPLAN Notices, vol.\u00a047, pp. 495\u2013508. ACM (2012)","DOI":"10.1145\/2103621.2103715"},{"key":"52_CR18","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"4","key":"52_CR19","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1002\/smr.316","volume":"17","author":"T. Mens","year":"2005","unstructured":"Mens, T., Eetvelde, N.V., Demeyer, S., Janssens, D.: Formalizing refactorings with graph transformations. Journal of Software Maintenance\u00a017(4), 247\u2013276 (2005)","journal-title":"Journal of Software Maintenance"},{"key":"52_CR20","unstructured":"Opdyke, W.F.: Refactoring object-oriented frameworks. PhD thesis, Champaign, IL, USA (1992)"},{"key":"52_CR21","doi-asserted-by":"crossref","unstructured":"Stevens, P.: A landscape of bidirectional model transformations. In: L\u00e4mmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol.\u00a05235, pp. 408\u2013424. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-88643-3_10"},{"key":"52_CR22","first-page":"172","volume-title":"ICSE 2006: Proceedings of the 28th International Conference on Software Engineering","author":"M. Verbaere","year":"2006","unstructured":"Verbaere, M., Ettinger, R., de Moor, O.: JunGL: a scripting language for refactoring. In: Rombach, D., Soffa, M.L. (eds.) ICSE 2006: Proceedings of the 28th International Conference on Software Engineering, pp. 172\u2013181. ACM Press, New York (2006)"},{"key":"52_CR23","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.T. Wenzel","year":"1999","unstructured":"Wenzel, M.T.: 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)"},{"key":"52_CR24","unstructured":"Whiteside, I.: Refactoring Proofs. PhD thesis, University of Edinburgh (2013)"},{"key":"52_CR25","doi-asserted-by":"crossref","unstructured":"Whiteside, I., Aspinall, D., Dixon, L., Grov, G.: Towards formal proof script refactoring. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS (LNAI), vol.\u00a06824, pp. 260\u2013275. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22673-1_18"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_52","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,18]],"date-time":"2022-03-18T20:33:43Z","timestamp":1647635623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}