{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T05:10:09Z","timestamp":1749877809883,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522272"},{"type":"electronic","value":"9783319522289"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-52228-9_10","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T04:23:43Z","timestamp":1484022223000},"page":"197-216","source":"Crossref","is-referenced-by-count":4,"title":["UTPCalc \u2014 A Calculator for UTP Predicates"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Butterfield","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18779-0","volume-title":"The Munich Project CIP, Volume II: The Program Transformation System CIP-S","author":"FL Bauer","year":"1987","unstructured":"Bauer, F.L., Ehler, H., Horsch, A., M\u00f6ller, B., Partsch, H., Paukner, O., Pepper, P.: The Munich Project CIP, Volume II: The Program Transformation System CIP-S. LNCS, vol. 292. Springer, Heidelberg (1987). doi: 10.1007\/3-540-18779-0"},{"key":"10_CR2","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","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":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"10_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781316092415","volume-title":"Thinking Functionally with Haskell","author":"R Bird","year":"2014","unstructured":"Bird, R.: Thinking Functionally with Haskell. Cambridge University Press, Cambridge (2014)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Butterfield, A.: Saoith\u00edn: a theorem prover for UTP. In: Proceedings of Unifying Theories of Programming - Third International Symposium, UTP 2010, Shanghai, China, 15\u201316 November 2010, pp. 137\u2013156 (2010). http:\/\/dx.doi.org\/10.1007\/978-3-642-16690-7_6","DOI":"10.1007\/978-3-642-16690-7_6"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Butterfield, A.: The logic of $$U \\cdot (TP)^{2}$$ . In: Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, 27\u201328 August 2012, Revised Selected Papers, pp. 124\u2013143 (2012). http:\/\/dx.doi.org\/10.1007\/978-3-642-35705-3_6","DOI":"10.1007\/978-3-642-35705-3_6"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Butterfield, A., Mjeda, A., Noll, J.: UTP semantics for shared-state, concurrent, context-sensitive process models. In: Bonsangue, M., Deng, Y. (eds.) TASE 2016 10th International Symposium on Theoretical Aspects of Software Engineering, pp. 93\u2013100, IEEE, July 2016","DOI":"10.1109\/TASE.2016.22"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76\u201387. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44881-0_7"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Foster, S., Woodcock, J.: Mechanised theory engineering in isabelle. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 246\u2013287. IOS Press (2015). http:\/\/dx.doi.org\/10.3233\/978-1-61499-495-4-246","DOI":"10.3233\/978-1-61499-495-4-246"},{"key":"10_CR9","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":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-59451-5_3","volume-title":"Advanced Functional Programming","author":"J Hughes","year":"1995","unstructured":"Hughes, J.: The design of a pretty-printing library. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 53\u201396. Springer, Heidelberg (1995). doi: 10.1007\/3-540-59451-5_3 . http:\/\/www.cs.chalmers.se\/~rjmh\/Papers\/pretty.ps"},{"key":"10_CR11","unstructured":"Marlow, S. (ed.): Haskell 2010 Language Report. Haskell Community (2010). https:\/\/www.haskell.org\/definition\/haskell2010.pdf"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). http:\/\/link.springer.de\/link\/service\/series\/0558\/tocs\/t2283.htm"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11768173_13","volume-title":"Unifying Theories of Programming","author":"G Nuka","year":"2006","unstructured":"Nuka, G., Woodcock, J.: Mechanising a unifying theory. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 217\u2013235. Springer, Heidelberg (2006). doi: 10.1007\/11768173_13"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0031813","volume-title":"Formal Methods in Computer-Aided Design","author":"N Shankar","year":"1996","unstructured":"Shankar, N.: PVS: combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 257\u2013264. Springer, Heidelberg (1996). doi: 10.1007\/BFb0031813"},{"issue":"4","key":"10_CR15","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1145\/567097.567099","volume":"24","author":"MGJ Brand Van Den","year":"2002","unstructured":"Van Den Brand, M.G.J., Heering, J., Klint, P., Olivier, P.A.: Compiling language definitions: the ASF+SDF compiler. ACM Trans. Program. Lang. Syst. 24(4), 334\u2013368 (2002)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45127-7_27","volume-title":"Rewriting Techniques and Applications","author":"E Visser","year":"2001","unstructured":"Visser, E.: Stratego: a language for program transformation based on rewriting strategies system description of stratego 0.5. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357\u2013361. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45127-7_27"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Wadler, P.: A prettier printer. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming (Cornerstones of Computing), Chap. 11, pp. 223\u2013244, Palgrave - Macmillan, March 2003","DOI":"10.1007\/978-1-349-91518-7_11"},{"key":"10_CR18","unstructured":"Wenzel, M.: The Isabelle\/Isar reference manual, June 2010. http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle\/doc\/isar-ref.pdf"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/11877028_15","volume-title":"Generative and Transformational Techniques in Software Engineering","author":"V Winter","year":"2006","unstructured":"Winter, V., Beranek, J.: Program transformation using HATS 1.84. In: L\u00e4mmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 378\u2013396. Springer, Heidelberg (2006). doi: 10.1007\/11877028_15"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-36103-0_5","volume-title":"Formal Methods and Software Engineering","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Hughes, A.: Unifying theories of parallel programming. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 24\u201337. Springer, Heidelberg (2002). doi: 10.1007\/3-540-36103-0_5"},{"key":"10_CR21","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.entcs.2009.05.055","volume":"240","author":"F Zeyda","year":"2009","unstructured":"Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Electr. Notes Theor. Comput. Sci. 240, 239\u2013257 (2009). http:\/\/dx.doi.org\/ 10.1016\/j.entcs.2009.05.055","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-52228-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T04:47:09Z","timestamp":1749876429000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52228-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522272","9783319522289"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52228-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}