{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:25Z","timestamp":1762459405656},"publisher-location":"Cham","reference-count":29,"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_17","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T02:11:57Z","timestamp":1474423917000},"page":"295-314","source":"Crossref","is-referenced-by-count":19,"title":["Unifying Heterogeneous State-Spaces with Lenses"],"prefix":"10.1007","author":[{"given":"Simon","family":"Foster","sequence":"first","affiliation":[]},{"given":"Frank","family":"Zeyda","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The Verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 209\u2013224. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-87873-5_18"},{"issue":"2","key":"17_CR2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/s00165-015-0343-1","volume":"28","author":"A Armstrong","year":"2015","unstructured":"Armstrong, A., Gomes, V., Struth, G.: Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28(2), 265\u2013293 (2015)","journal-title":"Formal Aspects Comput."},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-642-39634-2_16","volume-title":"Interactive Theorem Proving","author":"A Armstrong","year":"2013","unstructured":"Armstrong, A., Struth, G., Weber, T.: Program analysis and verification based on Kleene algebra in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 197\u2013212. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39634-2_16"},{"doi-asserted-by":"crossref","unstructured":"Back, R.-J., Preoteasa, V.: Reasoning about recursive procedures with parameters. In: Proceedings of the Workshop on Mechanized Reasoning About Languages with Variable Binding, MERLIN 2003, pp. 1\u20137. ACM (2003)","key":"17_CR4","DOI":"10.1145\/976571.976573"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-24364-6_2","volume-title":"Frontiers of Combining Systems","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic proof and disproof in Isabelle\/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 12\u201327. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24364-6_2"},{"doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366\u2013378. IEEE, July 2007","key":"17_CR6","DOI":"10.1109\/LICS.2007.30"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220\u2013268. Springer, Heidelberg (2006). doi: 10.1007\/11889229_6"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-19797-5_7","volume-title":"Mathematics of Program Construction","author":"B Dongol","year":"2015","unstructured":"Dongol, B., Gomes, V.B.F., Struth, G.: A program construction and verification tool for separation logic. In: Hinze, R., Voigtl\u00e4nder, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 137\u2013158. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19797-5_7"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-16690-7_9","volume-title":"Unifying Theories of Programming","author":"A Feliachi","year":"2010","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying theories in Isabelle\/HOL. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 188\u2013206. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16690-7_9"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-27705-4_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Feliachi","year":"2012","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle\/Circus: a process specification and verification environment. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243\u2013260. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-27705-4_20"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-19797-5_10","volume-title":"Mathematics of Program Construction","author":"S Fischer","year":"2015","unstructured":"Fischer, S., Hu, Z., Pacheco, H.: A clear picture of lens laws. In: Hinze, R., Voigtl\u00e4nder, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 215\u2013223. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19797-5_10"},{"unstructured":"Foster, J.: Bidirectional programming languages. Ph.D. thesis, University of Pennsylvania (2009)","key":"17_CR12"},{"issue":"3","key":"17_CR13","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1232420.1232424","volume":"29","author":"J Foster","year":"2007","unstructured":"Foster, J., Greenwald, M., Moore, J., Pierce, B., Schmitt, A.: Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), 17 (2007). doi: 10.1145\/1232420.1232424","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-21070-9_5","volume-title":"Relational and Algebraic Methods in Computer Science","author":"S Foster","year":"2011","unstructured":"Foster, S., Struth, G., Weber, T.: Automated engineering of relational and algebraic methods in Isabelle\/HOL. In: Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 52\u201367. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21070-9_5"},{"doi-asserted-by":"crossref","unstructured":"Foster, S., Thiele, B., Cavalcanti, A., Woodcock, J.: Towards a UTP semantics for Modelica. In Proceedings of the 6th International Symposium on Unifying Theories of Programming, June 2016. To appear","key":"17_CR15","DOI":"10.1007\/978-3-319-52228-9_3"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-14806-9_2","volume-title":"Unifying Theories of Programming","author":"S Foster","year":"2015","unstructured":"Foster, S., Zeyda, F., Woodcock, J.: Isabelle\/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21\u201341. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-14806-9_2"},{"key":"17_CR17","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8596-5","volume-title":"A Practical Theory of Programming","author":"ECR Hehner","year":"1993","unstructured":"Hehner, E.C.R.: A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer, New York (1993)"},{"key":"17_CR18","volume-title":"Cylindric Algebras, Part I","author":"L Henkin","year":"1971","unstructured":"Henkin, L., Monk, J., Tarski, A.: Cylindric Algebras, Part I. North-Holland, Amsterdam (1971)"},{"key":"17_CR19","volume-title":"Communicating Sequential Processes","author":"T Hoare","year":"1985","unstructured":"Hoare, T.: Communicating Sequential Processes. Prentice-Hall, London (1985)"},{"issue":"8","key":"17_CR20","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"T Hoare","year":"1987","unstructured":"Hoare, T., Hayes, I., He, J., Morgan, C., Roscoe, A., Sanders, J., S\u00f8rensen, I., Spivey, J., Sufrin, B.: The laws of programming. Commun. ACM 30(8), 672\u2013687 (1987)","journal-title":"Commun. ACM"},{"key":"17_CR21","volume-title":"Unifying Theories of Programming","author":"T Hoare","year":"1998","unstructured":"Hoare, T., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-03545-1_9"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., et\u00a0al.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM (2009)","key":"17_CR23","DOI":"10.1145\/1629575.1629596"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11768173_8","volume-title":"Unifying Theories of Programming","author":"M Oliveira","year":"2006","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 123\u2013140. Springer, Heidelberg (2006). doi: 10.1007\/11768173_8"},{"key":"17_CR26","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21, 3\u201332 (2009)","journal-title":"Formal Aspects Comput."},{"unstructured":"Schirmer, N., Wenzel, M.: State spaces - the locale way. In: SSV 2009. ENTCS, vol. 254, pp. 161\u2013179 (2009)","key":"17_CR27"},{"doi-asserted-by":"crossref","unstructured":"Woodcock, J., Foster, S., Butterfield, A.: Heterogeneous semantics and unifying theories. In: 7th International Symposium on Leveraging Applications of Formal Methods, Verification, and Validation (ISoLA) (2016). To appear","key":"17_CR28","DOI":"10.1007\/978-3-319-47166-2_26"},{"doi-asserted-by":"crossref","unstructured":"Zeyda, F., Foster, S., Freitas, L.: An axiomatic value model for Isabelle\/UTP. In: Proceedings of the 6th International Symposium on Unifying Theories of Programming (2016). To appear","key":"17_CR29","DOI":"10.1007\/978-3-319-52228-9_8"}],"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_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T20:29:53Z","timestamp":1568406593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}