{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:16:50Z","timestamp":1725484610576},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431664"},{"type":"electronic","value":"9783540456483"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45648-1_5","type":"book-chapter","created":{"date-parts":[[2007,5,28]],"date-time":"2007-05-28T01:26:02Z","timestamp":1180315562000},"page":"82-99","source":"Crossref","is-referenced-by-count":10,"title":["Encoding Object-Z in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Graeme","family":"Smith","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Kamm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Santen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,1,22]]},"reference":[{"key":"5_CR1","unstructured":"H. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, 1992."},{"issue":"5\u20136","key":"5_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"J. Bowen","year":"1995","unstructured":"J. Bowen and M. Gordon. A shallow embedding of Z in HOL. Information and Software Technology, 37(5\u20136):269\u2013276, 1995.","journal-title":"Information and Software Technology"},{"key":"5_CR3","unstructured":"M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"5_CR4","unstructured":"A. Griffiths. A Formal Semantics to Support Modular Reasoning in Object-Z. PhD thesis, University of Queensland, 1997."},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"A. Griffiths. Object-oriented operations have two parts. In D.J. Duke and A.S. Evans, editors, 2nd BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer-Verlag, 1997.","DOI":"10.14236\/ewic\/FA1997.10"},{"key":"5_CR6","unstructured":"F. Kamm\u00fcller. Modular Reasoning in Isabelle. PhD thesis, Computer Laboratory, University of Cambridge, 1999. Technical Report 470."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","first-page":"283","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs 96)","author":"K. T. Santen","year":"1996","unstructured":"Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle\/ HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics (TPHOLs 96), volume 1125 of Lecture Notes in Computer Science, pages 283\u2013298. Springer-Verlag, 1996."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BFb0028398","volume-title":"Theorem Proving in Higher-Order Logics (TPHOLs 97)","author":"T. Santen","year":"1997","unstructured":"T. Santen. A theory of structured model-based specifications in Isabelle\/HOL. In E.L. Gunter and A. Felty, editors, Theorem Proving in Higher-Order Logics (TPHOLs 97), volume 1275 of Lecture Notes in Computer Science, pages 243\u2013258. Springer-Verlag, 1997."},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/BFb0056028","volume-title":"ZUM\u201998: The Z Formal Specification Notation","author":"T. Santen","year":"1998","unstructured":"T. Santen. On the semantic relation of Z and HOL. In J. Bowen and A. Fett, editors, ZUM\u201998: The Z Formal Specification Notation, LNCS 1493, pages 96\u2013115. Springer-Verlag, 1998."},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-48256-3_4","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Santen","year":"1999","unstructured":"T. Santen. Isomorphisms-a link between the shallow and the deep. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Th\u00e9ry, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 37\u201354. Springer-Verlag, 1999."},{"key":"5_CR12","unstructured":"T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. Shaker-Verlag, 2000. Dissertation, Fachbereich Informatik, Technische Universit\u00e4t Berlin, (1999)."},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"G. Smith. The Object-Z Specification Language. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"5_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-44525-0_4","volume-title":"Recursive schema definitions in Object-Z","author":"G. Smith","year":"2000","unstructured":"G. Smith. Recursive schema definitions in Object-Z. In A. Galloway J. Bowen, S. Dunne and S. King, editors, International Conference of B and Z Users (ZB 2000), volume 1878 of Lecture Notes in Computer Science, pages 42\u201358. Springer-Verlag, 2000."},{"key":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-63533-5_17","volume-title":"Formal Methods Europe (FME 97)","author":"H. Tej","year":"1997","unstructured":"H. Tej and B. Wolff. A corrected failure-divergence model for CSP in Isabelle\/HOL. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Formal Methods Europe (FME 97), volume 1313 of Lecture Notes in Computer Science, pages 318\u2013337. Springer-Verlag, 1997."}],"container-title":["Lecture Notes in Computer Science","ZB 2002:Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45648-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T21:34:30Z","timestamp":1683840870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45648-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431664","9783540456483"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-45648-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}