{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:23:46Z","timestamp":1759638226792},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119569"},{"type":"electronic","value":"9783642119576"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_26","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"488-506","source":"Crossref","is-referenced-by-count":16,"title":["A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While"],"prefix":"10.1007","author":[{"given":"Keiko","family":"Nakata","sequence":"first","affiliation":[]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"26_CR1","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. of Automated Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"J. of Automated Reasoning"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science\u00a01(2), article 1 (2005)","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"26_CR3","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/143165.143184","volume-title":"Conf. Record of 19th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1992","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: Conf. Record of 19th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL 1992, Albuquerque, NM, January 1992, pp. 83\u201394. ACM Press, New York (1992)"},{"issue":"2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.ic.2008.03.025","volume":"207","author":"P. Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R.: Bi-inductive structural semantics. Inform. and Comput.\u00a0207(2), 258\u2013283 (2009)","journal-title":"Inform. and Comput."},{"key":"26_CR5","unstructured":"Danielsson, N.A., Altenkirch, T.: Mixing induction and coinduction. Draft (2009), \n                  \n                    http:\/\/www.cs.nott.ac.uk\/~nad\/publications\/"},{"key":"26_CR6","series-title":"Electron. Notes in Theor. Comput. Sci.","first-page":"73","volume-title":"Proc. of 3rd Int. Wksh. on Compiler Optimization Meets Compiler Verification, COCV 2004","author":"S. Glesner","year":"2004","unstructured":"Glesner, S.: A proof calculus for natural semantics based on greatest fixed point semantics. In: Knoop, J., Necula, G.C., Zimmermann, W. (eds.) Proc. of 3rd Int. Wksh. on Compiler Optimization Meets Compiler Verification, COCV 2004, Barcelona, April 2004. Electron. Notes in Theor. Comput. Sci., vol.\u00a0132(1), pp. 73\u201393. Elsevier, Amsterdam (2004)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/BFb0036915","volume-title":"Automata, Languages and Programming","author":"J. Halpern","year":"1983","unstructured":"Halpern, J., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 278\u2013291. Springer, Heidelberg (1983)"},{"issue":"4","key":"26_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.2168\/LMCS-3(4:11)2007","volume":"3","author":"I. Hasuo","year":"2007","unstructured":"Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Computer Science\u00a03(4), article 11 (2007)","journal-title":"Logical Methods in Computer Science"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78663-4_1","volume-title":"Trustworthy Global Computing","author":"M. Hofmann","year":"2008","unstructured":"Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol.\u00a04912, pp. 1\u201320. Springer, Heidelberg (2008)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11693024_5","volume-title":"Programming Languages and Systems","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Coinductive big-step operational semantics. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 54\u201368. Springer, Heidelberg (2006)"},{"issue":"2","key":"26_CR11","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inform. and Comput.\u00a0207(2), 285\u2013305 (2009)","journal-title":"Inform. and Comput."},{"issue":"5","key":"26_CR12","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T. Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Asp. Comput.\u00a011(5), 541\u2013566 (1999)","journal-title":"Formal Asp. Comput."},{"issue":"2","key":"26_CR13","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B. Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A temporal logic for reasoning about hardware. Computer\u00a018(2), 10\u201319 (1985)","journal-title":"Computer"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"TPHOLs 2009","author":"K. Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for While: big-step and small-step, relational and functional styles. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 375\u2013390. Springer, Heidelberg (2009)"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11784180_22","volume-title":"Algebraic Methodology and Software Technology","author":"H. Nestra","year":"2006","unstructured":"Nestra, H.: Fractional semantics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 278\u2013292. Springer, Heidelberg (2006)"},{"issue":"7","key":"26_CR16","doi-asserted-by":"crossref","first-page":"574","DOI":"10.1016\/j.jlap.2009.03.001","volume":"78","author":"H. Nestra","year":"2009","unstructured":"Nestra, H.: Transfinite semantics in the form of greatest fixpoint. J. of Logic and Algebr. Program.\u00a078(7), 574\u2013593 (2009)","journal-title":"J. of Logic and Algebr. Program."},{"key":"26_CR17","volume-title":"Semantics with Applications: A Formal Introduction","author":"H. Riis Nielson","year":"1992","unstructured":"Riis Nielson, H., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley, Chichester (1992)"},{"issue":"4-5","key":"26_CR18","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1051\/ita:1999125","volume":"33","author":"J. Rutten","year":"1999","unstructured":"Rutten, J.: A note on coinduction and weak bisimilarity for While programs. Theor. Inform. and Appl.\u00a033(4-5), 393\u2013400 (1999)","journal-title":"Theor. Inform. and Appl."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:46Z","timestamp":1606185946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}