{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:50:59Z","timestamp":1781927459236,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710653","type":"print"},{"value":"9783540710677","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71067-7_14","type":"book-chapter","created":{"date-parts":[[2008,10,3]],"date-time":"2008-10-03T08:55:16Z","timestamp":1223024116000},"page":"134-149","source":"Crossref","is-referenced-by-count":63,"title":["Imperative Functional Programming with Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Lukas","family":"Bulwahn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander","family":"Krauss","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Haftmann","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Levent","family":"Erk\u00f6k","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Matthews","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"R.S. Boyer","year":"2002","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol.\u00a02257, pp. 9\u201327. Springer, Heidelberg (2002)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Een","year":"2004","unstructured":"Een, N., S\u00f6rensson, N.: An extensible sat-solver. In: Goos, G., Hartmanis, J., van Leeuwen, J. (eds.) SAT 2003. LNCS, vol.\u00a02919, p. 502. Springer, Heidelberg (2004)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590. Springer, Heidelberg (2007)"},{"key":"14_CR4","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. Technical Report 364\/07, Department of Computer Science, University of Kaiserslautern (August 2007)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11541868_10","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Huffman","year":"2005","unstructured":"Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle\/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 147\u2013162. Springer, Heidelberg (2005)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Jones, S.P., Launchbury, J.: Lazy functional state threads. In: SIGPLAN Conference on Programming Language Design and Implementation, pp. 24\u201335 (1994)","DOI":"10.1145\/773473.178246"},{"issue":"4","key":"14_CR7","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst.\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-47813-2_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Krsti\u0107","year":"2002","unstructured":"Krsti\u0107, S., Matthews, J.: Verifying BDD algorithms through monadic interpretation. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 182\u2013195. Springer, Heidelberg (2002)"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1017\/S095679689900341X","volume":"9","author":"O. M\u00fcller","year":"1999","unstructured":"M\u00fcller, O., Nipkow, T., Oheimb, D.V., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming\u00a09, 191\u2013223 (1999)","journal-title":"Journal of Functional Programming"},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1145\/1159803.1159812","volume-title":"ICFP 2006: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming","author":"A. Nanevski","year":"2006","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in hoare type theory. In: ICFP 2006: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, pp. 62\u201373. ACM Press, New York (2006)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/11921240_19","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"S. Obua","year":"2006","unstructured":"Obua, S.: Partizan games in Isabelle\/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 272\u2013286. Springer, Heidelberg (2006)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Jones, S.P., Wadler, P.: Imperative functional programming. In: Proc. 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1993), pp. 71\u201384 (1993)","DOI":"10.1145\/158511.158524"},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-74591-4_23","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Sprenger","year":"2007","unstructured":"Sprenger, C., Basin, D.A.: A monad-based modeling and verification toolbox with application to security protocols. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 302\u2013318. Springer, Heidelberg (2007)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, January 2007, pp. 97\u2013108 (2007)","DOI":"10.1145\/1190216.1190234"},{"key":"14_CR17","unstructured":"Weber, T., Amjad, H.: Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic (to appear, 2007)"}],"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\/978-3-540-71067-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T07:49:31Z","timestamp":1557820171000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71067-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710653","9783540710677"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71067-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}