{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:55Z","timestamp":1725488635222},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_4","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"37-54","source":"Crossref","is-referenced-by-count":2,"title":["Isomorphisms \u2014 A Link Between the Shallow and the Deep"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Santen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"issue":"5","key":"4_CR1","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"},{"issue":"4","key":"4_CR2","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471\u2013522, 1985.","journal-title":"Computing Surveys"},{"key":"4_CR3","series-title":"Lect Notes Comput Sci","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":"M. Gordon. Set theory, higher order logic or both? In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, LNCS 1125, pages 191\u2013201. Springer-Verlag, 1996."},{"key":"4_CR4","unstructured":"M. J. C. Gordon and T. M. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"4_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BFb0053566","volume-title":"Programming Languages and Systems-7th European Symposium on Programming, ESOP\u201998","author":"U. Hensel","year":"1998","unstructured":"U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In C. Hankin, editor, Programming Languages and Systems-7th European Symposium on Programming, ESOP\u201998, LNCS 1381, pages 105\u2013121. Springer-Verlag, 1998."},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. A. R. Hoare","year":"1972","unstructured":"C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher-Order Logics","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, LNCS 1125, pages 283\u2013298. Springer-Verlag, 1996."},{"key":"4_CR8","unstructured":"L. Lamport and L. C. Paulson. Should your specification language be typed? \n                  http:\/\/www.cl.cam.ac.uk\/users\/lcp\/papers\/lamport-paulson-types.ps.gz\n                  \n                , 1997."},{"key":"4_CR9","unstructured":"B. Meyer. Reusable Software. Prentice Hall, 1994."},{"key":"4_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0055145","volume-title":"Theorem Proving in Higher Order Logics","author":"O. M\u00fcller","year":"1998","unstructured":"O. M\u00fcller. I\/O automata and beyond: temporal logic and abstraction in Isabelle. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, LNCS 1479, pages 331\u2013348. Springer-Verlag, 1998."},{"issue":"10","key":"4_CR11","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1093\/comjnl\/40.10.640","volume":"40","author":"O. M\u00fcller","year":"1997","unstructured":"O. M\u00fcller and K. Slind. Treating partiality in a logic of total functions. The Computer Journal, 40(10):640\u2013651, 1997.","journal-title":"The Computer Journal"},{"key":"4_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/BFb0055146","volume-title":"Theorem Proving in Higher Order Logics \u2014 11th International Conference, TPHOLs\u201998","author":"W. Naraschewski","year":"1998","unstructured":"W. Naraschewski and M. Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics \u2014 11th International Conference, TPHOLs\u201998, LNCS 1479, pages 349\u2013366. Springer-Verlag, 1998."},{"key":"4_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1007\/3-540-61511-3_125","volume-title":"Automated Deduction \u2014 CADE 14","author":"T. Nipkow","year":"1996","unstructured":"T. Nipkow. More Church\/Rosser proofs (in Isabelle\/HOL). In Automated Deduction \u2014 CADE 14, LNCS 1104, pages 733\u2013747. Springer-Verlag, 1996."},{"key":"4_CR14","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Laboratory, 1993."},{"key":"4_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle\u2013A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle\u2013A Generic Theorem Prover. LNCS 828. Springer-Verlag, 1994."},{"key":"4_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BFb0028398","volume-title":"Proc. International Conference on Theorem Proving in Higher Order Logics","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, Proc. International Conference on Theorem Proving in Higher Order Logics, LNCS 1275, pages 243\u2013258. Springer-Verlag, 1997."},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/978-3-540-49676-2_8","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":"4_CR18","unstructured":"T. Santen. A Mechanized Logical Model of Z and Object-Oriented Specification. PhDthesis, Fachbereich Informatik, Technische Universit\u00e4t Berlin, Germany, 1999. forthcoming."},{"key":"4_CR19","unstructured":"J. M. Spivey. The Z Notation \u2014 A Reference Manual. Prentice Hall, 2nd edition, 1992."},{"key":"4_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-63533-5_17","volume-title":"FME\u201997: Industrial Applications and Strengthened Foundations of Formal Methods","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, FME\u201997: Industrial Applications and Strengthened Foundations of Formal Methods, LNCS 1313, pages 318\u2013337. Springer-Verlag, 1997."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T22:52:17Z","timestamp":1550443937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}