{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:15Z","timestamp":1767929295872,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540330950","type":"print"},{"value":"9783540330967","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11693024_5","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T13:30:35Z","timestamp":1143552635000},"page":"54-68","source":"Crossref","is-referenced-by-count":22,"title":["Coinductive Big-Step Operational Semantics"],"prefix":"10.1007","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0304-3975(98)00135-2","volume":"212","author":"A. Berarducci","year":"1999","unstructured":"Berarducci, A., Dezani-Ciancaglini, M.: Infinite lambda-calculus and types. Theor. Comp. Sci.\u00a0212(1-2), 29\u201375 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"5_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":"5_CR3","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"5_CR4","first-page":"83","volume-title":"19th symp. Principles of Progr. Lang.","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: 19th symp. Principles of Progr. Lang., pp. 83\u201394. ACM Press, New York (1992)"},{"issue":"6","key":"5_CR5","doi-asserted-by":"crossref","first-page":"511","DOI":"10.1017\/S0956796802004318","volume":"12","author":"V. Gapeyev","year":"2003","unstructured":"Gapeyev, V., Levin, M., Pierce, B.: Recursive subtyping revealed. J. Func. Progr.\u00a012(6), 511\u2013548 (2003)","journal-title":"J. Func. Progr."},{"key":"5_CR6","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":"5_CR7","unstructured":"Grall, H.: Deux crit\u00e8res de s\u00e9curit\u00e9 pour l\u00e9x\u00e9cution de code mobile. PhD thesis, \u00c9cole Nationale des Ponts et Chauss\u00e9es (December 2003)"},{"key":"5_CR8","unstructured":"Gr\u00e9goire, B.: Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml. PhD thesis, University Paris 7 (2003)"},{"key":"5_CR9","unstructured":"Gunter, C.A., R\u00e9my, D.: A proof-theoretic assessment of runtime type errors. Research Report 11261-921230-43TM, AT&T Bell Laboratories (1993)"},{"issue":"2","key":"5_CR10","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796898002986","volume":"8","author":"T. Hardin","year":"1998","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional runtimes within the lambdasigma calculus. Journal of Functional Programming\u00a08(2), 131\u2013176 (1998)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"5_CR11","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(96)00171-5","volume":"175","author":"R. Kennaway","year":"1997","unstructured":"Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.-J.: Infinitary lambda calculus. Theor. Comp. Sci.\u00a0175(1), 93\u2013125 (1997)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR12","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia (March 2004) (To appear in ACM TOPLAS)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Coinductive big-step operational semantics \u2013 the Coq development (2005), Available from pauillac.inria.fr\/~xleroy","DOI":"10.1007\/11693024_5"},{"key":"5_CR14","first-page":"42","volume-title":"33rd symp. Principles of Progr. Lang.","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symp. Principles of Progr. Lang., pp. 42\u201354. ACM Press, New York (2006)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-48749-2_7","volume-title":"Secure Internet Programming","author":"X. Leroy","year":"1999","unstructured":"Leroy, X., Rouaix, F.: Security properties of typed applets. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol.\u00a01603, pp. 147\u2013182. Springer, Heidelberg (1999)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R. Milner","year":"1991","unstructured":"Milner, R., Tofte, M.: Co-induction in relational semantics. Theor. Comp. Sci.\u00a087, 209\u2013220 (1991)","journal-title":"Theor. Comp. Sci."},{"key":"5_CR17","unstructured":"Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, G\u00f6teborg University (1988)"},{"key":"5_CR18","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II)","author":"A. Stoughton","year":"1998","unstructured":"Stoughton, A.: An operational semantics framework supporting the incremental construction of derivation trees. In: Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II). Electronic Notes in Theoretical Computer Science, vol.\u00a012, Elsevier, Amsterdam (1998)"},{"key":"5_CR19","unstructured":"Strecker, M.: Compiler verification for C0. Technical report, Universit\u00e9 Paul Sabatier, Toulouse (April 2005)"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. and Comp.\u00a0115(1), 38\u201394 (1994)","journal-title":"Inf. and Comp."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11693024_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,13]],"date-time":"2020-04-13T11:38:03Z","timestamp":1586777883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11693024_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540330950","9783540330967"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11693024_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}