{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:37:03Z","timestamp":1754483823748},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540620341"},{"type":"electronic","value":"9783540496311"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-62034-6_48","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:31:54Z","timestamp":1330295514000},"page":"180-192","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Winskel is (almost) right"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Y. Bertot and R. Fraer. Reasoning with executable specifications. In TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lect. Notes in Comp. Sci., pages 531\u2013545. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59293-8_218"},{"key":"16_CR2","unstructured":"M. Gordon. Programming Language Theory and its Implementation. Prentice-Hall, 1988."},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"M. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_10"},{"key":"16_CR4","unstructured":"M. Gordon and T. Melham. Introduction to HOL: a theorem-proving environment for higher-order logic. Cambridge University Press, 1993."},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"P. V. Homeier and D. F. Martin. Trustworthy tools for trustworthy programs: A verified verification condition generator. In T. Melham and J. Camilleri, editors, Higher Order Logic Theorem Proving and its Applications, volume 859 of Lect. Notes in Comp. Sci., pages 269\u2013284. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_48"},{"key":"16_CR6","unstructured":"H. L\u00f6tzbeyer and R. Sandner. Proof of the equivalence of the operational and denotational semantics of IMP in Isabelle\/ZF. Project report, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1994."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Logic and Computation. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"16_CR9","unstructured":"L. C. Paulson. Generic automatic proof tools. Technical Report 396, University of Cambridge, Computer Laboratory, 1996."},{"key":"16_CR10","unstructured":"F. Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische Universit\u00c4t M\u00fcnchen, 1994."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"F. Regensburger. HOLCF: Higher Order Logic of Computable Functions. In E. Schubert, P. Windley, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lect. Notes in Comp. Sci., pages 293\u2013307. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_72"},{"key":"16_CR12","unstructured":"L. van Benthem Jutting. Checking Landau's \u201cGrundlagen\u201d in the AUTOMATH System. PhD thesis, Eindhoven University of Technology, 1977."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-62034-6_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T11:08:37Z","timestamp":1640948917000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62034-6_48"}},"subtitle":["Towards a mechanized semantics textbook"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540620341","9783540496311"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-62034-6_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}