{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:10:23Z","timestamp":1754485823187,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_17","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"216-232","source":"Crossref","is-referenced-by-count":15,"title":["Animating the Formalised Semantics of a Java-Like Language"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]},{"given":"Lukas","family":"Bulwahn","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-68103-8_2","volume-title":"Types for Proofs and Programs","author":"R. Atkey","year":"2008","unstructured":"Atkey, R.: CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"17_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management","author":"C. Ballarin","year":"2006","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: Theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 31\u201343. Springer, Heidelberg (2006)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-92188-2_1","volume-title":"Formal Methods for Components and Objects","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, G., Nipkow, T.: Flyspeck I: Tame graphs. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (2006), http:\/\/afp.sourceforge.net\/entries\/Flyspeck-Tame.shtml , Formal proof development","DOI":"10.1007\/11814771_4"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-03359-9_11","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Berghofer","year":"2009","unstructured":"Berghofer, S., Bulwahn, L., Haftmann, F.: Turning inductive into equational specifications. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 131\u2013146. Springer, Heidelberg (2009)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 134\u2013149. Springer, Heidelberg (2008)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-27815-3_14","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Bevilacqua, V., Ro\u015fu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 147\u2013150. Springer, Heidelberg (2004)"},{"key":"17_CR8","unstructured":"Haftmann, F.: Data refinement (raffinement) in Isabelle\/HOL This is a draft of an envisaged publication still to be elaborated which, applying the usual rules of academic confidentiality, can be inspected at, http:\/\/www4.in.tum.de\/~haftmann\/pdf\/data_refinement_haftmann.pdf"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F. Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 103\u2013117. Springer, Heidelberg (2010)"},{"key":"17_CR10","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. Progr. Lang. Sys.\u00a028, 619\u2013695 (2006)","journal-title":"ACM Trans. Progr. Lang. Sys."},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The Isabelle Collections Framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"issue":"4","key":"17_CR12","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"17_CR14","first-page":"15","volume-title":"IVME 2003","author":"H. Liu","year":"2003","unstructured":"Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: A study. In: IVME 2003, pp. 15\u201323. ACM, New York (2003)"},{"key":"17_CR15","unstructured":"Lochbihler, A.: Type safe nondeterminism \u2013 a formal semantics of Java threads. In: Workshop on Foundations of Object-Oriented Languages, FOOL 2008 (2008)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-642-11957-6_23","volume-title":"Programming Languages and Systems","author":"A. Lochbihler","year":"2010","unstructured":"Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 427\u2013447. Springer, Heidelberg (2010)"},{"key":"17_CR17","unstructured":"Lochbihler, A.: Jinja with threads. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs (2007), http:\/\/afp.sourceforge.net\/entries\/JinjaThreads.shtml , Formal proof development"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-03359-9_22","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Lochbihler","year":"2009","unstructured":"Lochbihler, A.: Formalising FinFuns \u2013 generating code for functions as data from Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 310\u2013326. Springer, Heidelberg (2009)"},{"issue":"50","key":"17_CR19","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F. Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci.\u00a0411(50), 4333\u20134356 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 452\u2013468. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:39Z","timestamp":1560449619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}