{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:46Z","timestamp":1725467506191},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055146","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"349-366","source":"Crossref","is-referenced-by-count":24,"title":["Object-oriented verification based on record subtyping in Higher-Order Logic"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Naraschewski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Wenzel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"21_CR1","unstructured":"P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986."},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56\u201368, 1940.","DOI":"10.2307\/2266170"},{"key":"21_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":"21_CR4","doi-asserted-by":"crossref","unstructured":"U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about classes in object-oriented languages: Logical models and tools. In Proceedings of ESOP\/ETAPS, volume 1381 of Lecture Notes in Computer Science. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0053566"},{"issue":"1","key":"21_CR5","first-page":"51","volume":"4","author":"M. Hofmann","year":"1998","unstructured":"M. Hofmann, W. Naraschewski, M. Steffen, and T. Stroup. Inheritance of proofs. Theory and Practice of Object Systems, Special Issue on Third Workshop on Foundations of Object-Oriented Languages (FOOL 3), 4(1):51\u201369, 1998.","journal-title":"Theory and Practice of Object Systems, Special Issue on Third Workshop on Foundations of Object-Oriented Languages (FOOL 3)"},{"key":"21_CR6","unstructured":"L. Lamport and L. C. Paulson. Should your specification language be typed? Technical Report 425, University of Cambridge Computer Laboratory, 1997."},{"issue":"3","key":"21_CR7","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1145\/44501.45065","volume":"10","author":"J. C. Mitchell","year":"1988","unstructured":"J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. ACM Trans. Prog. Lang. Syst., 10(3):470\u2013502, July 1988.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"21_CR8","unstructured":"W. Naraschewski. Object-Oriented Proof Principles using the Proof-Assistant Lego. Diplomarbeit, Universit\u00c4t Erlangen, 1996."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"W. Naraschewski. Towards an object-oriented progification language. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, volume 1275 of Lecture Notes in Computer Science, pages 215\u2013230. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0028396"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"issue":"2","key":"21_CR11","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1017\/S0956796800001040","volume":"4","author":"B. C. Pierce","year":"1994","unstructured":"B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207\u2013247, 1994.","journal-title":"Journal of Functional Programming"},{"key":"21_CR12","unstructured":"A. Pitts. The HOL logic. In Gordon and Melham [3], pages 191\u2013232."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"M. Wenzel. Type classes and overloading in higher-order logic. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs'97, volume 1275 of Lecture Notes in Computer Science, pages 307\u2013322. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0028402"}],"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\/BFb0055146","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:33:51Z","timestamp":1555734831000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055146"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0055146","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}