Skip to main content
SpringerLink
Log in
Book cover

European Conference on Object-Oriented Programming

ECOOP 2014: ECOOP 2014 – Object-Oriented Programming pp 282–307Cite as

Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8586))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)

    Article  Google Scholar 

  2. 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

  3. 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)

    Chapter  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Google Scholar 

  6. Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theor. Inf. and Applic. 45(1), 3–33 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Intersection and union types: Syntax and semantics. Information and Computation 119(2), 202–230 (1995)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. Brandt, M., Henglein, F.: Coinductive axiomatization of recursive type equality and subtyping. Fundam. Inform. 33(4), 309–338 (1998)

    MATH  MathSciNet  Google Scholar 

  11. Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  12. Frisch, A., Castagna, G., Benzaken, V.: Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. J. ACM 55(4) (2008)

    Google Scholar 

  13. Hosoya, H., Pierce, B.C.: XDuce: A statically typed XML processing language. ACM Trans. Internet Techn. 3(2), 117–148 (2003)

    Article  Google Scholar 

  14. Hosoya, H., Vouillon, J., Pierce, B.C.: Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27(1), 46–90 (2005)

    Article  Google Scholar 

  15. Igarashi, A., Nagira, H.: Union types for object-oriented programming. Journ. of Object Technology 6(2), 47–68 (2007)

    Article  Google Scholar 

  16. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207, 284–304 (2009)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIBRIS, Università di Genova, Italy

    Davide Ancona & Andrea Corradi

Authors
  1. Davide Ancona
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrea Corradi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Kent, Canterbury, Kent, UK

    Richard Jones

1 Electronic Supplementary Material

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation