Skip to main content
SpringerLink
Log in

Preciseness of Subtyping on Intersection and Union Types

  • Conference paper
Rewriting and Typed Lambda Calculi (RTA 2014, TLCA 2014)

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

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 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 that describes 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.

We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We then prove soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness.

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

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

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

    Article  MATH  MathSciNet  Google Scholar 

  3. Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48(4), 931–940 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  4. Blackburn, J., Hernandez, I., Ligatti, J., Nachtigal, M.: Completely Subtyping Iso-recursive Types. Technical Report CSE-071012, University of South Florida (2012)

    Google Scholar 

  5. Boudol, G.: Lambda-calculi for (Strict) Parallel Functions. Information and Computation 108(1), 51–127 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  6. Castagna, G., De Nicola, R., Varacca, D.: Semantic Subtyping for the Pi-calculus. Theoretical Computer Science 398(1-3), 217–242 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  7. Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Padovani, L.: Foundations of Session Types. In: López-Fraguas, F.J. (ed.) PPDP, pp. 219–230. ACM (2009)

    Google Scholar 

  8. Chen, T.-C., Dezani-Ciancaglini, M., Yoshida, N.: On the Preciseness of Subtyping in Session Types (2014), http://www.di.unito.it/~dezani/papers/cdy14.pdf

  9. Dezani-Ciancaglini, M., de’ Liguoro, U., Piperno, A.: A Filter Model for Concurrent lambda-Calculus. SIAM Journal on Computing 27(5), 1376–1419 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  10. Dezani-Ciancaglini, M., Frisch, A., Giovannetti, E., Motohama, Y.: The Relevance of Semantic Subtyping. In: van Bakel, S. (ed.) ITRS. ENTCS, vol. 70(1), pp. 88–105 (2002)

    Google Scholar 

  11. Dunfield, J.: Elaborating Intersection and Union Types. In: Thiemann, P., Findler, R.B. (eds.) ICFP, pp. 17–28. ACM (2012)

    Google Scholar 

  12. Frisch, A., Castagna, G., Benzaken, V.: Semantic Subtyping. In: Plotkin, G. (ed.) LICS, pp. 137–146. IEEE (2002)

    Google Scholar 

  13. Frisch, A., Castagna, G., Benzaken, V.: Semantic Subtyping: Dealing set-theoretically with Function, Union, Intersection, and Negation Types. Journal of ACM 55(4) (2008)

    Google Scholar 

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

    Google Scholar 

  15. Hindley, J.R.: The Completeness Theorem for Typing Lambda-Terms. Theoretical Computer Science 22, 1–17 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  16. Ishihara, H., Kurata, T.: Completeness of Intersection and Union Type Assignment Systems for Call-by-value Lambda-models. Theoretical Computer Science 272(1-2), 197–221 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  17. de’ Liguoro, U., Piperno, A.: Non Deterministic Extensions of Untyped Lambda-Calculus. Information and Computation 122(2), 149–177 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  18. Mitchell, J.C.: Polymorphic Type Inference and Containment. Information and Computation 76(2/3), 211–249 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  19. Ong, C.-H.L.: Non-Determinism in a Functional Setting. In: Vardi, M.Y. (ed.) LICS, pp. 275–286. IEEE (1993)

    Google Scholar 

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

    Google Scholar 

  21. Plotkin, G.D.: Call-by-name, Call-by-value and the λ-calculus. Theoretical Computer Science 1(2), 125–159 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  22. Routley, R., Meyer, R.K.: The Semantics of Entailment III. Journal of Philosophical Logic 1, 192–208 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  23. Tiuryn, J., Urzyczyn, P.: The Subtyping Problem for Second-Order Types is Undecidable. Information and Computation 179(1), 1–18 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  24. Urzyczyn, P.: The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64(3), 1195–1215 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  25. 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. Dipartimento di Informatica, Università di Torino, Italy

    Mariangiola Dezani-Ciancaglini

  2. Faculty of Technical Sciences, University of Novi Sad, Serbia

    Silvia Ghilezan

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

Editor information

Editors and Affiliations

  1. Inria, 23 avenue d’Italie, CS 81321, 75214, Paris Cedex 13, France

    Gilles Dowek

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Dezani-Ciancaglini, M., Ghilezan, S. (2014). Preciseness of Subtyping on Intersection and Union Types. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08918-8_14

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08917-1

  • Online ISBN: 978-3-319-08918-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation