Abstract
Structural subtyping is an important notion for effective static type analysis; it can be defined either axiomatically by a collection of subtyping rules, or by means of set inclusion between type interpretations, following the more intuitive approach of semantic subtyping, which allows simpler proofs of the expected properties of the subtyping relation.
In object-oriented programming, recursive types are typically interpreted inductively; however, cyclic objects can be represented more precisely by coinductive types.
We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming, and develop and implement a sound and complete top-down direct and effective algorithm for deciding it. To our knowledge, this is the first proposal for a sound and complete top-down direct algorithm for semantic subtyping between coinductive types.
Partly funded by the project MIUR CINA - Compositionality, Interaction, Negotiation, Autonomicity for the future ICT society.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Ancona, D., Corradi, A.: Sound and complete subtyping between coinductive types for object-oriented languages. Technical report, DIBRIS - Università di Genova, Italy (2014), ftp://ftp.disi.unige.it/person/AnconaD/CompleteCoinductiveSubtyping.pdf
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é, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 31–45. Springer, Heidelberg (2011)
Ancona, D., Lagorio, G.: Coinductive type systems for object-oriented languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 2–26. Springer, Heidelberg (2009)
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. 25, pp. 214–223 (2010)
Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theor. Inf. and Applic. 45(1), 3–33 (2011)
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. 7604, pp. 10–27. Springer, Heidelberg (2012)
Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Intersection and union types: Syntax and semantics. Information and Computation 119(2), 202–230 (1995)
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)
Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inform. 33(4), 309–338 (1998)
Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)
Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55(4) (2008)
Hosoya, H., Pierce, B.C.: XDuce: A statically typed XML processing language. ACM Trans. Internet Techn. 3(2), 117–148 (2003)
Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27(1), 46–90 (2005)
Igarashi, A., Nagira, H.: Union types for object-oriented programming. Journ. of Object Technology 6(2), 47–68 (2007)
Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207, 284–304 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
1 Electronic Supplementary Material
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ancona, D., Corradi, A. (2014). Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages. In: Jones, R. (eds) ECOOP 2014 – Object-Oriented Programming. ECOOP 2014. Lecture Notes in Computer Science, vol 8586. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44202-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-662-44202-9_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44201-2
Online ISBN: 978-3-662-44202-9
eBook Packages: Computer ScienceComputer Science (R0)