{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T19:20:27Z","timestamp":1794424827442,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642310560","type":"print"},{"value":"9783642310577","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31057-7_21","type":"book-chapter","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T07:17:41Z","timestamp":1340867861000},"page":"459-483","source":"Crossref","is-referenced-by-count":9,"title":["Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics"],"prefix":"10.1007","author":[{"given":"Davide","family":"Ancona","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11506676_16","volume-title":"Logic Based Program Synthesis and Transformation","author":"M.S. Ager","year":"2005","unstructured":"Ager, M.S.: From Natural Semantics to Abstract Machines. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol.\u00a03573, pp. 245\u2013261. Springer, Heidelberg (2005)"},{"issue":"4","key":"21_CR2","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1145\/155183.155231","volume":"15","author":"R. Amadio","year":"1993","unstructured":"Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems\u00a015(4), 575\u2013631 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Ancona, D.: Coinductive big-step operational semantics for type soundness of Java-like languages. In: Formal Techniques for Java-like Programs (FTfJP 2011), pp. 5:1\u20135:6. ACM (2011)","DOI":"10.1145\/2076674.2076679"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-18070-5_3","volume-title":"Formal Verification of Object-Oriented Software","author":"D. Ancona","year":"2011","unstructured":"Ancona, D., Corradi, A., Lagorio, G., Damiani, F.: Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification? In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 31\u201345. Springer, Heidelberg (2011)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-03013-0_2","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"D. Ancona","year":"2009","unstructured":"Ancona, D., Lagorio, G.: Coinductive Type Systems for Object-Oriented Languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 2\u201326. Springer, Heidelberg (2009)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Ancona, D., Lagorio, G.: Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas. In: Montanari, A., Napoli, M., Parente, M. (eds.) Proceedings of GandALF 2010. Electronic Proceedings in Theoretical Computer Science, vol.\u00a025, pp. 214\u2013223 (2010)","DOI":"10.4204\/EPTCS.25.20"},{"issue":"1","key":"21_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1051\/ita\/2011009","volume":"45","author":"D. Ancona","year":"2011","unstructured":"Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theoretical Informatics and Applications\u00a045(1), 3\u201333 (2011)","journal-title":"RAIRO - Theoretical Informatics and Applications"},{"key":"21_CR8","doi-asserted-by":"crossref","first-page":"445","DOI":"10.3233\/FI-1980-3405","volume":"3","author":"A. Arnold","year":"1980","unstructured":"Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae\u00a03, 445\u2013476 (1980)","journal-title":"Fundamenta Informaticae"},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","volume":"25","author":"B. Courcelle","year":"1983","unstructured":"Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science\u00a025, 95\u2013169 (1983)","journal-title":"Theoretical Computer Science"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: POPL, pp. 270\u2013282 (2006)","DOI":"10.1145\/1111320.1111062"},{"issue":"3","key":"21_CR11","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/503502.503505","volume":"23","author":"A. Igarashi","year":"2001","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems\u00a023(3), 396\u2013450 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1-4","key":"21_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.3233\/FI-2010-323","volume":"103","author":"J.D.M. Kusmierek","year":"2010","unstructured":"Kusmierek, J.D.M., Bono, V.: Big-step operational semantics revisited. Fundam. Inform.\u00a0103(1-4), 137\u2013172 (2010)","journal-title":"Fundam. Inform."},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"284","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. Information and Computation\u00a0207, 284\u2013304 (2009)","journal-title":"Information and Computation"},{"issue":"1","key":"21_CR14","first-page":"209","volume":"87","author":"M. Tofte","year":"1990","unstructured":"Tofte, M., Milner, R.: Co-induction in relational semantics. Theoretical Computer Science\u00a087(1), 209\u2013220 (1990)","journal-title":"Theoretical Computer Science"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-Based Coinductive Operational Semantics for While. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 375\u2013390. Springer, Heidelberg (2009)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K. Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 488\u2013506. Springer, Heidelberg (2010)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/11799573_25","volume-title":"Logic Programming","author":"L. Simon","year":"2006","unstructured":"Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive Logic Programming. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079, pp. 330\u2013345. Springer, Heidelberg (2006)"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Stoughton, A.: An operational semantics framework supporting the incremental construction of derivation trees. Electr. Notes Theor. Comput. Sci.\u00a010 (1997)","DOI":"10.1016\/S1571-0661(05)80693-0"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2012 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31057-7_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,19]],"date-time":"2022-01-19T15:32:09Z","timestamp":1642606329000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31057-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642310560","9783642310577"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31057-7_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-31057-7","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}