{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:26:46Z","timestamp":1784255206602,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_26","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"375-390","source":"Crossref","is-referenced-by-count":26,"title":["Trace-Based Coinductive Operational Semantics for While"],"prefix":"10.1007","author":[{"given":"Keiko","family":"Nakata","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Coq\u2019Art: Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11417170_9","volume-title":"Typed Lambda Calculi and Applications","author":"Y. Bertot","year":"2005","unstructured":"Bertot, Y.: Filters on coinductive streams, an application to Eratosthenes\u2019 sieve. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 102\u2013115. Springer, Heidelberg (2005)"},{"key":"26_CR3","unstructured":"Bertot, Y.: A survey of programming language semantics styles. Coq development (2007), \n                    \n                      http:\/\/www-sop.inria.fr\/marelle\/Yves.Bertot\/proofs.html"},{"issue":"2","key":"26_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-1(2:1)2005","volume":"1","author":"V. Capretta","year":"2005","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science\u00a01(2), 1\u201318 (2005)","journal-title":"Logical Methods in Computer Science"},{"key":"26_CR5","first-page":"83","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, pp. 83\u201394. ACM Press, New York (1992)"},{"issue":"2","key":"26_CR6","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_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-60579-7_3","volume-title":"Types for Proofs and Programs","author":"E. Gim\u00e9nez","year":"1995","unstructured":"Gim\u00e9nez, E.: Codifying guarded definitions with recursive schemes. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996, pp. 39\u201359. Springer, Heidelberg (1995)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E. Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 397\u2013408. Springer, Heidelberg (1998)"},{"key":"26_CR9","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":"2005","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. Electron. Notes in Theor. Comput. Sci., vol.\u00a0132(1), pp. 73\u201393. Elsevier, Amsterdam (2005)"},{"key":"26_CR10","series-title":"Electron. Notes in Theor. Comput. Sci.","first-page":"61","volume-title":"Proc. of 5th Int. Wksh. on Compiler Optimization Meets Compiler Verification, COCV\u00a02006","author":"S. Glesner","year":"2007","unstructured":"Glesner, S., Leitner, J., Blech, J.O.: Coinductive verification of program optimizations using similarity relations. In: Knoop, J., Necula, G.C., Zimmermann, W. (eds.) Proc. of 5th Int. Wksh. on Compiler Optimization Meets Compiler Verification, COCV\u00a02006, Vienna. Electron. Notes in Theor. Comput. Sci., vol.\u00a0176(3), pp. 61\u201377. Elsevier, Amsterdam (2007)"},{"key":"26_CR11","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. Technical Report RR-6455, INRIA (2008)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Comput. Sci.\u00a03(4), article 11(2007)","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"26_CR13","unstructured":"Leroy, X.: The Compcert verified compiler. Commented Coq development (2008), \n                    \n                      http:\/\/compcert.inria.fr\/doc\/"},{"issue":"2","key":"26_CR14","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."},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C. McBride","year":"2002","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 197\u2013216. Springer, Heidelberg (2002)"},{"key":"26_CR16","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 semantic. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, pp. 278\u2013292. Springer, Heidelberg (2006)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Nestra, H.: Transfinite semantics in the form of greatest fixpoint. J. of Logic and Algebr. Program (to appear)","DOI":"10.1016\/j.jlap.2009.03.001"},{"issue":"4\u20135","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\u20135), 393\u2013400 (1999)","journal-title":"Theor. Inform. and Appl."}],"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-642-03359-9_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T09:08:34Z","timestamp":1552122514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}