{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T06:40:23Z","timestamp":1759992023648},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540347507"},{"type":"electronic","value":"9783540347521"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11768173_13","type":"book-chapter","created":{"date-parts":[[2006,6,21]],"date-time":"2006-06-21T12:02:49Z","timestamp":1150891369000},"page":"217-235","source":"Crossref","is-referenced-by-count":7,"title":["Mechanising a Unifying Theory"],"prefix":"10.1007","author":[{"given":"Gift","family":"Nuka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"R.-J. Back","year":"1990","unstructured":"Back, R.-J., von Wright, J.: Refinement concepts formalised in higher order logic. Formal Asp. Comput.\u00a02(3), 247\u2013272 (1990)","journal-title":"Formal Asp. Comput."},{"key":"13_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J.J. Back","year":"1998","unstructured":"Back, R.-J.J., Akademi, A., Von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998)"},{"issue":"5\u20136","key":"13_CR3","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J.P. Bowen","year":"1995","unstructured":"Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Information and Software Technology\u00a037(5\u20136), 269\u2013276 (1995)","journal-title":"Information and Software Technology"},{"key":"13_CR4","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-1-4471-3452-7_9","volume-title":"Z User Workshop, Cambridge 1994","author":"J.P. Bowen","year":"1994","unstructured":"Bowen, J.P., Gordon, M.J.C.: Z and HOL. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge 1994. Workshops in Computing, pp. 141\u2013167. Springer, Heidelberg (1994)"},{"key":"13_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn De","year":"1972","unstructured":"De Bruijn, N.G.: Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Indag Math.\u00a034, 381\u2013392 (1972)","journal-title":"Indag Math."},{"key":"13_CR6","series-title":"Discrete Mathematics and Theoretical Computer Science","first-page":"40","volume-title":"Formal Methods Pacific 1997: Proceedings of FMP 1997","author":"M. Butler","year":"1997","unstructured":"Butler, M., Grundy, J., L\u00e5ngbacka, T., Ruk\u0161\u0117nas, R., von Wright, J.: The refinement calculator: Proof support for program refinement. In: Groves, L., Reeves, S. (eds.) Formal Methods Pacific 1997: Proceedings of FMP 1997, Wellington, New Zealand. Discrete Mathematics and Theoretical Computer Science, pp. 40\u201361. Springer, Heidelberg (1997)"},{"issue":"9","key":"13_CR7","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1109\/32.58786","volume":"16","author":"A.J. Camilleri","year":"1990","unstructured":"Camilleri, A.J.: Mechamising CSP Trace Theory in Higher Order Logic. IEEE Transactions on Software Engineering\u00a016(9), 88\u2013118 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR8","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"13_CR9","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical aspects of computer science: Proc. American Mathematics Soc. symposia","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Mathematical aspects of computer science: Proc. American Mathematics Soc. symposia, vol.\u00a019, pp. 19\u201331. American Mathematical Society, Providence RI (1967)"},{"key":"13_CR10","first-page":"214","volume-title":"LICS 1999: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science","author":"M. Gabbay","year":"1999","unstructured":"Gabbay, M., Pitts, A.: A new approach to abstract syntax involving binders. In: LICS 1999: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, p. 214. IEEE Computer Society, Los Alamitos (1999)"},{"key":"13_CR11","first-page":"387","volume-title":"Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification)","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G.M., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), Banff, Canada, pp. 387\u2013439. Springer, Berlin (1988)"},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/69610.357988","volume":"27","author":"E.C.R. Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming part i. Commun. ACM\u00a027(2), 134\u2013143 (1984)","journal-title":"Commun. ACM"},{"issue":"2","key":"13_CR13","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/69610.357990","volume":"27","author":"E.C.R. Hehner","year":"1984","unstructured":"Hehner, E.C.R.: Predicative programming part ii. Commun. ACM\u00a027(2), 144\u2013151 (1984)","journal-title":"Commun. ACM"},{"issue":"10","key":"13_CR14","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"13_CR15","volume-title":"Programs are predicates","author":"C.A. Hoare","year":"1984","unstructured":"Hoare, C.A.: Programs are predicates. Prentice-Hall, Englewood Cliffs (1984)"},{"key":"13_CR16","volume-title":"Unifying Theories of Programming","author":"C.A.R. Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)"},{"key":"13_CR17","volume-title":"Object-oriented software engineering with Eiffel","author":"J.-M. Jezequel","year":"1996","unstructured":"Jezequel, J.-M.: Object-oriented software engineering with Eiffel. Addison Wesley Longman Publishing Co., Inc., Redwood City (1996)"},{"issue":"9","key":"13_CR18","first-page":"423","volume":"6","author":"R.D. Maddux","year":"1991","unstructured":"Maddux, R.D.: The origin of relation algebras in the development and axiomatization of the calculus of relations. Studia Logica\u00a06(9), 423\u2013455 (1991)","journal-title":"Studia Logica"},{"key":"13_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"S. Maharaj","year":"1994","unstructured":"Maharaj, S.: Enconding Z-style schemas in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806. Springer, Heidelberg (1994)"},{"issue":"1","key":"13_CR20","first-page":"50","volume":"1","author":"T.F. Melham","year":"1994","unstructured":"Melham, T.F.: A Mechanized Theory of the \u03c0-calculus in HOL. Nordic Journal of Computing\u00a01(1), 50\u201376 (1994)","journal-title":"Nordic Journal of Computing"},{"key":"13_CR21","volume-title":"Introduction to HOL: A Theorem proving Environment for Higher Order Logic","author":"R. Milner","year":"1993","unstructured":"Milner, R., Goldon, M.J.C.: Introduction to HOL: A Theorem proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"13_CR22","volume-title":"Programming from specifications","author":"C. Morgan","year":"1990","unstructured":"Morgan, C.: Programming from specifications. Prentice-Hall Inc., Upper Saddle River (1990)"},{"key":"13_CR23","unstructured":"Morgan, C.C., Sanders, J.W.: Laws of the Logical calculi. Technical Report PRG-78. Programming Research group, Oxford, England (1989)"},{"issue":"4","key":"13_CR24","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"Nelson, G.: A Generalization of Dijkstra\u2019s calculus. ACM Trans. Program. Lang. Syst.\u00a011(4), 517\u2013561 (1989)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-62034-6_48","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Nipkow","year":"1996","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol.\u00a01180, pp. 180\u2013192. Springer, Heidelberg (1996)"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.entcs.2004.04.013","volume":"95","author":"G. Nuka","year":"2004","unstructured":"Nuka, G., Woodcock, J.: Mechanising the alphabetised relational calculus. Electr. Notes Theor. Comput. Sci.\u00a095, 209\u2013225 (2004)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR27","volume-title":"Isabelle - A generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle - A generic Theorem Prover. Springer, Heidelberg (1994)"},{"issue":"2","key":"13_CR28","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"A.M. Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation\u00a0186(2), 165\u2013193 (2003)","journal-title":"Information and Computation"},{"key":"13_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45614-7_26","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"A. Sampaio","year":"2002","unstructured":"Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 451\u2013470. Springer, Heidelberg (2002)"},{"issue":"9","key":"13_CR31","doi-asserted-by":"crossref","first-page":"73","DOI":"10.2307\/2268577","volume":"6","author":"A. Tarski","year":"1941","unstructured":"Tarski, A.: On the calculus of relations. Journal of Symbolic Logic\u00a06(9), 73\u201389 (1941)","journal-title":"Journal of Symbolic Logic"},{"key":"13_CR32","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantics of programming languages: an introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The formal semantics of programming languages: an introduction. MIT Press, Cambridge (1993)"},{"key":"13_CR33","volume-title":"Using Z Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Unifying Theories of Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11768173_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:06:43Z","timestamp":1605643603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11768173_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540347507","9783540347521"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11768173_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}