Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Denotational and Operational Preciseness of Subtyping: A Roadmap

Dedicated to Frank de Boer on the Occasion of His 60th Birthday

  • Chapter
  • First Online:
Theory and Practice of Formal Methods

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9660))

Abstract

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in object-oriented programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: denotational and operational. The former preciseness is based on the denotation of a type, which is a mathematical object describing the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected.

The present paper shows that standard proofs of operational preciseness imply denotational preciseness and gives an overview on this subject.

Partly supported by COST IC1201 BETTY and DART bilateral project between Italy and Serbia.

M. Dezani-Ciancaglini—Partly supported by EU H2020-644235 Rephrase project, EU H2020-644298 HyVar project, ICT COST Actions IC1402 ARVI and Ateneo/CSP project RunVar.

S. Ghilezan et al.—Partly supported by ON 174026 and III 44006 projects of the Ministry of Education, Science and Technological Development, Republic of Serbia.

N. Yoshida—Partly supported by EPSRC EP/K011715/1, EP/K034413/1, and EP/L00058X/1, and EU Project FP7-612985 UpScale.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 EPUB and 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

Institutional subscriptions

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, New York (1996)

    Book  MATH  Google Scholar 

  2. van Bakel, S., Dezani-Ciancaglini, M., de’ Liguoro, U., Motohama, Y.: The minimal relevant logic and the call-by-value lambda calculus. Technical Report TR-ARP-05-2000, The Australian National University (2000)

    Google Scholar 

  3. Barbanera, F., de Liguoro, U.: Two notions of sub-behaviour for session-based client/server systems. In: Kutsia, T., Schreiner, W., Fernández, M. (eds.) PPDP, pp. 155–164. ACM (2010)

    Google Scholar 

  4. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48(4), 931–940 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bernardi, G., Dardha, O., Gay, S.J., Kouzapas, D.: On duality relations for session types. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 51–66. Springer, Heidelberg (2014)

    Google Scholar 

  6. Bonsangue, M.M., Rot, J., Ancona, D., de Boer, F.S., Rutten, J.J.M.M.: A coalgebraic foundation for coinductive union types. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014, Part II. LNCS, vol. 8573, pp. 62–73. Springer, Heidelberg (2014)

    Google Scholar 

  7. Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330–349. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Castagna, G., De Nicola, R., Varacca, D.: Semantic subtyping for the pi-calculus. Theoret. Comput. Sci. 398(1–3), 217–242 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  9. Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of session types. In: PPDP, pp. 219–230. ACM (2009)

    Google Scholar 

  10. Castagna, G., Frisch, A.: A gentle introduction to semantic subtyping. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 30–34. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Chen, T.-C., Dezani-Ciancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: Chitil, O., King, A., Danvy, O. (eds.) PPDP, pp. 135–146. ACM Press (2014)

    Google Scholar 

  12. Coppo, M., Dezani-Ciancaglini, M., Padovani, L., Yoshida, N.: A gentle introduction to multiparty asynchronous session types. In: Bernardo, M., Johnsen, E.B. (eds.) SFM 2015. LNCS, vol. 9104, pp. 146–178. Springer, Switzerland (2015)

    Google Scholar 

  13. Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Dezani-Ciancaglini, M., de ’Liguoro, U., Piperno, A.: A filter model for concurrent lambda-calculus. SIAM J. Comput. 27(5), 1376–1419 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  15. Dezani-Ciancaglini, M., Ghilezan, S.: Preciseness of subtyping on intersection and union types. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 194–207. Springer, Heidelberg (2014)

    Google Scholar 

  16. Dezani-Ciancaglini, M., Ghilezan, S., Jaksic, S., Pantovic, J., Yoshida, N.: Precise subtyping for synchronous multiparty sessions. In: PLACES, EPTCS 203, pp. 29–44 (2016)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  18. Gay, S.J.: Bounded polymorphism in session types. Math. Struct. Comput. Sci. 18(5), 895–930 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  19. Goto, M., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible approach to session polymorphism. Math. Struct. Comput. Sci. 26(3), 465–509 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  20. Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press, Cambridge (2013)

    MATH  Google Scholar 

  21. Hindley, J.R.: The completeness theorem for typing lambda-terms. Theoret. Comput. Sci. 22, 1–17 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  22. Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  23. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In POPL, pp. 273–284. ACM (2008). A full version will appear in Journal of the Association for Computing Machinery

    Google Scholar 

  24. Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoret. Comput. Sci. 311(1–3), 121–163 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  25. Ishihara, H., Kurata, T.: Completeness of intersection and union type assignment systems for call-by-value lambda-models. Theoret. Comput. Sci. 272(1–2), 197–221 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  26. Kouzapas, D., Yoshida, N.: Globally governed session semantics. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 395–409. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  27. Ligatti, J., Blackburn, J., Nachtigal, M.: On subtyping-relation completeness, with an application to iso-recursive types. Technical report, University of South Florida (2014)

    Google Scholar 

  28. Mitchell, J.C.: Polymorphic type inference and containment. Inf. Comput. 76(2/3), 211–249 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  29. Mostrous, D.: Session Types in Concurrent Calculi: Higher-Order Processes and Objects. PhD thesis, Imperial College London (2009)

    Google Scholar 

  30. Mostrous, D., Yoshida, N.: Session-based communication optimisation for higher-order mobile processes. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 203–218. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Mostrous, D., Yoshida, N.: Session typing and asynchronous subtyping for the higher-order \(\pi \)-calculus. Inf. Comput. 241, 227–263 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  32. Mostrous, D., Yoshida, N., Honda, K.: Global principal typing in partially commutative asynchronous sessions. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 316–332. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Padovani, L.: Fair subtyping for multi-party session types. In: De Meuter, W., Roman, G.-C. (eds.) COORDINATION 2011. LNCS, vol. 6721, pp. 127–141. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  34. Padovani, L.: Fair subtyping for open session types. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 373–384. Springer, Heidelberg (2013)

    Google Scholar 

  35. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    Google Scholar 

  36. Tiuryn, J., Urzyczyn, P.: The subtyping problem for second-order types is undecidable. Inf. Comput. 179(1), 1–18 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  37. Urzyczyn, P.: The emptiness problem for intersection types. J. Symbolic Logic 64(3), 1195–1215 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  38. Vouillon, J.: Subtyping union types. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 415–429. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Università di Torino, Turin, Italy

    Mariangiola Dezani-Ciancaglini

  2. Univerzitet u Novom Sadu, Novi Sad, Serbia

    Silvia Ghilezan, Svetlana Jakšić & Jovanka Pantović

  3. Imperial College London, London, UK

    Nobuko Yoshida

Authors
  1. Mariangiola Dezani-Ciancaglini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Silvia Ghilezan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Svetlana Jakšić
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jovanka Pantović
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Nobuko Yoshida
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nobuko Yoshida .

Editor information

Editors and Affiliations

  1. Informatik 2, RWTH Aachen University Informatik 2, Aachen, Germany

    Erika Ábrahám

  2. Leiden University , Leiden, The Netherlands

    Marcello Bonsangue

  3. University of Oslo , Oslo, Norway

    Einar Broch Johnsen

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this chapter

Cite this chapter

Dezani-Ciancaglini, M., Ghilezan, S., Jakšić, S., Pantović, J., Yoshida, N. (2016). Denotational and Operational Preciseness of Subtyping: A Roadmap. In: Ábrahám, E., Bonsangue, M., Johnsen, E. (eds) Theory and Practice of Formal Methods. Lecture Notes in Computer Science(), vol 9660. Springer, Cham. https://doi.org/10.1007/978-3-319-30734-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30734-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30733-6

  • Online ISBN: 978-3-319-30734-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation