{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:05Z","timestamp":1759638905921},"publisher-location":"Cham","reference-count":25,"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_8","type":"book-chapter","created":{"date-parts":[[2017,1,9]],"date-time":"2017-01-09T23:23:43Z","timestamp":1484004223000},"page":"155-175","source":"Crossref","is-referenced-by-count":3,"title":["An Axiomatic Value Model for Isabelle\/UTP"],"prefix":"10.1007","author":[{"given":"Frank","family":"Zeyda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Foster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leo","family":"Freitas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"JC Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 116\u2013130. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_11"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-16690-7_6","volume-title":"Unifying Theories of Programming","author":"A Butterfield","year":"2010","unstructured":"Butterfield, A.: Saoith\u00edn: a theorem prover for UTP. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 137\u2013156. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16690-7_6"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-35705-3_6","volume-title":"Unifying Theories of Programming","author":"A Butterfield","year":"2013","unstructured":"Butterfield, A.: The logic of $$\\mathit{U}\\cdot (\\mathit{TP})^{2}$$ . In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 124\u2013143. Springer, Berlin (2013). doi: 10.1007\/978-3-642-35705-3_6"},{"issue":"1","key":"8_CR4","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s00165-012-0253-4","volume":"25","author":"A Cavalcanti","year":"2013","unstructured":"Cavalcanti, A., Wellings, A., Woodcock, J.: The safety-critical java memory model formalised. Formal Aspects Comput, 25(1), 37\u201357 (2013)","journal-title":"Formal Aspects Comput,"},{"key":"8_CR5","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"},{"doi-asserted-by":"publisher","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: a process specification and verification environment. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243\u2013260. Springer, Berlin (2012). doi: 10.1007\/978-3-642-27705-4_20","key":"8_CR6","DOI":"10.1007\/978-3-642-27705-4_20"},{"key":"8_CR7","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":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BFb0105405","volume-title":"Theorem Proving in Higher Order Logics","author":"M Gordon","year":"1996","unstructured":"Gordon, M.: Set theory, higher order logic or both? In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 191\u2013201. Springer, Heidelberg (1996). doi: 10.1007\/BFb0105405"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"MJ Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979)"},{"unstructured":"Hoare, T., Jifeng, H.: Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall, Upper Saddle River (1998). http:\/\/www.unifyingtheories.org\/","key":"8_CR10"},{"issue":"Special Issue 0","key":"8_CR11","doi-asserted-by":"crossref","first-page":"883","DOI":"10.1017\/S0960129511000144","volume":"21","author":"M Iancu","year":"2011","unstructured":"Iancu, M., Rabe, F.: Formalising foundations of mathematics. Math. Struct. Comput. Sci. 21(Special Issue 04), 883\u2013911 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-319-22102-1_16","volume-title":"Interactive Theorem Proving","author":"O Kun\u010dar","year":"2015","unstructured":"Kun\u010dar, O., Popescu, A.: A consistent foundation for Isabelle\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 234\u2013252. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-22102-1_16"},{"key":"8_CR13","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, Berlin (2002). 3540433767"},{"key":"8_CR14","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":"8_CR15","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"},{"unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for . Formal Aspects Comput. 21(1), 3\u201332 (2007)","key":"8_CR16"},{"issue":"1","key":"8_CR17","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s00165-007-0044-5","volume":"25","author":"M Oliveira","year":"2013","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. Formal Aspects Comput. 25(1), 133\u2013158 (2013)","journal-title":"Formal Aspects Comput."},{"unstructured":"Pitts, A.: Part III: The HOL Logic. In: Gordon, M.J.C., Melham, T.F. (eds) Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic, pp. 191\u2013232. Cambridge University Press, March 1993","key":"8_CR18"},{"unstructured":"RTCA, Inc.: Formal Methods Supplement to DO-178C and DO-278A. Technical report DO-333, RTCA, Washington, DC 20036, USA, December 2011","key":"8_CR19"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/11768173_2","volume-title":"Unifying Theories of Programming","author":"T Santos","year":"2006","unstructured":"Santos, T., Cavalcanti, A., Sampaio, A.: Object-orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 18\u201337. Springer, Heidelberg (2006). doi: 10.1007\/11768173_2"},{"issue":"2","key":"8_CR21","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A Sherif","year":"2010","unstructured":"Sherif, A., Cavalcanti, A., Jifeng, H., Sampaio, A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects Comput. 22(2), 153\u2013191 (2010)","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"8_CR22","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/BF01214920","volume":"8","author":"M Spivey","year":"2015","unstructured":"Spivey, M.: The consistency theorem for free type definitions in Z. Formal Aspects Comput. 8(3), 369\u2013375 (2015)","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (Co)datatypes for higher-order logic: category theory applied to theorem proving. In: Proceedings of LICS 2012, pp. 596\u2013605. IEEE, June 2012","key":"8_CR23","DOI":"10.1109\/LICS.2012.75"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-35705-3_10","volume-title":"Unifying Theories of Programming","author":"F Zeyda","year":"2013","unstructured":"Zeyda, F., Cavalcanti, A.: Higher-order UTP for a theory of methods. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 204\u2013223. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35705-3_10"},{"issue":"4","key":"8_CR25","doi-asserted-by":"crossref","first-page":"444","DOI":"10.1016\/j.scico.2010.02.010","volume":"77","author":"F Zeyda","year":"2012","unstructured":"Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Sci. Comput. Program. 77(4), 444\u2013479 (2012)","journal-title":"Sci. Comput. Program."}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T03:45:58Z","timestamp":1498362358000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52228-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522272","9783319522289"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52228-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}