{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,11]],"date-time":"2026-09-11T04:23:24Z","timestamp":1789100604508,"version":"build-2803163510"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662442012","type":"print"},{"value":"9783662442029","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44202-9_12","type":"book-chapter","created":{"date-parts":[[2014,7,16]],"date-time":"2014-07-16T22:01:13Z","timestamp":1405548073000},"page":"282-307","source":"Crossref","is-referenced-by-count":11,"title":["Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages"],"prefix":"10.1007","author":[{"given":"Davide","family":"Ancona","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Corradi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"4","key":"12_CR1","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":"12_CR2","doi-asserted-by":"crossref","unstructured":"Ancona, D., Corradi, A.: Sound and complete subtyping between coinductive types for object-oriented languages. Technical report, DIBRIS - Universit\u00e0 di Genova, Italy (2014), ftp:\/\/ftp.disi.unige.it\/person\/AnconaD\/CompleteCoinductiveSubtyping.pdf","DOI":"10.1007\/978-3-662-44202-9_12"},{"key":"12_CR3","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":"12_CR4","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":"12_CR5","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":"12_CR6","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 - Theor. Inf. and Applic.\u00a045(1), 3\u201333 (2011)","journal-title":"RAIRO - Theor. Inf. and Applic."},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-33475-7_2","volume-title":"Theoretical Computer Science","author":"D. Ancona","year":"2012","unstructured":"Ancona, D., Lagorio, G.: Static single information form for abstract compilation. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol.\u00a07604, pp. 10\u201327. Springer, Heidelberg (2012)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., de\u2019Liguoro, U.: Intersection and union types: Syntax and semantics. Information and Computation\u00a0119(2), 202\u2013230 (1995)","DOI":"10.1006\/inco.1995.1086"},{"key":"12_CR9","unstructured":"Bonsangue, M., Rot, J., Ancona, D., de Boer, F., Rutten, J.: A coalgebraic foundation for coinductive union types. In: 41st International Colloquium on Automata, Languages and Programming, ICALP 2014 (to appear, 2014)"},{"issue":"4","key":"12_CR10","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1998-33401","volume":"33","author":"M. Brandt","year":"1998","unstructured":"Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inform.\u00a033(4), 309\u2013338 (1998)","journal-title":"Fundam. Inform."},{"key":"12_CR11","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":"12_CR12","doi-asserted-by":"crossref","unstructured":"Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM\u00a055(4) (2008)","DOI":"10.1145\/1391289.1391293"},{"issue":"2","key":"12_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/767193.767195","volume":"3","author":"H. Hosoya","year":"2003","unstructured":"Hosoya, H., Pierce, B.C.: XDuce: A statically typed XML processing language. ACM Trans. Internet Techn.\u00a03(2), 117\u2013148 (2003)","journal-title":"ACM Trans. Internet Techn."},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/1053468.1053470","volume":"27","author":"H. Hosoya","year":"2005","unstructured":"Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. ACM Trans. Program. Lang. Syst.\u00a027(1), 46\u201390 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.5381\/jot.2007.6.2.a3","volume":"6","author":"A. Igarashi","year":"2007","unstructured":"Igarashi, A., Nagira, H.: Union types for object-oriented programming. Journ. of Object Technology\u00a06(2), 47\u201368 (2007)","journal-title":"Journ. of Object Technology"},{"key":"12_CR16","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"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2014 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44202-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,22]],"date-time":"2020-08-22T06:02:08Z","timestamp":1598076128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44202-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662442012","9783662442029"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44202-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}