Document Open Access Logo

Deconfined Intersection Types in Java

Authors Mariangiola Dezani-Ciancaglini , Paola Giannini , Betti Venneri

PDF
Thumbnail PDF

File

OASIcs.Gabbrielli.3.pdf
  • Filesize: 0.56 MB
  • 25 pages

Document Identifiers

Author Details

Mariangiola Dezani-Ciancaglini
  • Computer Science Department, University of Torino, Italy
Paola Giannini
  • Department of Advanced Science and Technology, University of Eastern Piedmont, Alessandria, Italy
Betti Venneri
  • Department of Statistics, Computer Science, Applications, University of Firenze, Italy

Acknowledgements

We are very pleased to dedicate this work to Maurizio, whose notable contributions to the theory of programming languages are well known and appreciated by the scientific community. We would like to thank the anonymous referees for their helpful comments.

Cite As Get BibTex

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Deconfined Intersection Types in Java. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/OASIcs.Gabbrielli.3

Abstract

We show how Java intersection types can be freed from their confinement in type casts, in such a way that the proposed Java extension is safe and fully compatible with the current language. To this aim, we exploit two calculi which formalise the simple Java core and the extended language, respectively. Namely, the second calculus extends the first one by allowing an intersection type to be used anywhere in place of a nominal type. We define a translation algorithm, compiling programs of the extended language into programs of the former calculus. The key point is the interaction between λ-expressions and intersection types, that adds safe expressiveness while being the crucial matter in the translation. We prove that the translation preserves typing and semantics. Thus, typed programs in the proposed extension are translated to typed Java programs. Moreover, semantics of translated programs coincides with the one of the source programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Semantics and reasoning
Keywords
  • Intersection Types
  • Featherweight Java
  • Lambda Expressions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  2. Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Java & Lambda: a Featherweight Story. Logical Methods in Computer Science, 14(3):1-24, 2018. URL: https://doi.org/10.23638/LMCS-14(3:17)2018.
  3. Viviana Bono, Betti Venneri, and Lorenzo Bettini. A Typed Lambda Calculus with Intersection Types. Theoretical Computer Science, 398(1-3):95-113, 2008. URL: https://doi.org/10.1016/j.tcs.2008.01.046.
  4. Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the Future Safe for the Past: Adding Genericity to the Java Programming Language. In Bjørn N. Freeman-Benson and Craig Chambers, editors, OOPSLA, pages 183-200. ACM Press, 1998. URL: https://doi.org/10.1145/286936.286957.
  5. Martin Büchi and Wolfgang Weck. Compound Types for Java. In Bjørn N. Freeman-Benson and Craig Chambers, editors, OOPSLA, pages 362-373. ACM Press, 1998. URL: https://doi.org/10.1145/286936.286975.
  6. Mario Coppo and Mariangiola Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. URL: https://doi.org/10.1305/ndjfl/1093883253.
  7. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal Type Schemes and λ-calculus Semantics. In To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 535-560. Academic Press, 1980. ISBN-13: 9780123490506. Google Scholar
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional Characters of Solvable Terms. Mathematical Logical Quartely, 27(2-6):45-58, 1981. URL: https://doi.org/10.1002/malq.19810270205.
  9. Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. A Core Calculus for Scala Type Checking. In Rastislav Kralovic and Pawel Urzyczyn, editors, MFCS, volume 4162 of LNCS, pages 1-23, Berlin, 2006. Springer. URL: https://doi.org/10.1007/11821069_1.
  10. Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Intersection Types in Java: Back to the Future. In Tiziana Margaria, Susanne Graf, and Kim G. Larsen, editors, Models, Mindsets, Meta: The What, the How, and the Why Not?, volume 11200 of LNCS, pages 68-86. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-22348-9_6.
  11. Andrej Dudenhefner and Jakob Rehof. Intersection Type Calculi of Bounded Dimension. In Giuseppe Castagna and Andrew D. Gordon, editors, POPL, pages 653-665. ACM Press, 2017. URL: https://doi.org/10.15520/jbme.v6i7.2243.
  12. Andrej Dudenhefner and Jakob Rehof. Typability in Bounded Dimension. In Joel Ouaknine, editor, LICS, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005127.
  13. Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Longman Publishing Co., Inc., 1995. ISBN-13: 0201633612. Google Scholar
  14. James Gosling, Bill Joy, Guy L. Steele, Gilad Bracha, and Alex Buckley. The Java Language Specification, Java SE 8 Edition. Oracle, 2015. ISBN-13: 9780133900699. Google Scholar
  15. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A Minimal Core Calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  16. Java 10, 2018. URL: https://docs.oracle.com/javase/10/language/toc.htm#JSLAN-GUID-7D5FDD65-ACE4-4B3C-80F4-CC01CBD211A4.
  17. Luigi Liquori and Simona Ronchi Della Rocca. Intersection-types à la Church. Information and Computation, 205(9):1371-1386, 2007. URL: https://doi.org/10.1016/j.ic.2007.03.005.
  18. Robert C. Martin. Agile Software Development: Principles, Patterns and Practices. Pearson Education, 2002. ISBN: 0-13-597444-5. Google Scholar
  19. Martin Odersky, Lex Spoon, and Bill Venners. Programming in Scala: Updated for Scala 2.12. Artima Incorporation, 3rd edition, 2016. ISBN-13: 9780981531687. Google Scholar
  20. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. ISBN: 0262162091. Google Scholar
  21. Garrel Pottinger. A Type Assignment for the Strongly Normalizable λ-terms. In To H.B.Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, pages 561-578. Academic Press, 1980. ISBN-13: 9780123490506. Google Scholar
  22. Marianna Rapoport, Ifaz Kabir, Paul He, and Ondrej Lhoták. A Simple Soundness Proof for Dependent Object Types. Proceedings of the ACM on Programming Languages, 1(OOPSLA):46:1-46:27, 2017. URL: https://doi.org/10.1145/3133870.
  23. John C. Reynolds. Conjunctive Types and Algol-like Languages. In David Gries, editor, LICS, page 119. IEEE Computer Society, 1987. Google Scholar
  24. John C. Reynolds. Design of the Programming Language Forsythe. In Algol-like Languages, Progress in Theoretical Computer Science, pages 173-233. Birkhäuser, 1997. ISBN-978-1-4612-8661-5. Google Scholar
  25. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and Andrew P. Black. Traits: Composable Units of Behaviour. In Luca Cardelli, editor, ECOOP, volume 2743 of LNCS, pages 248-274. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45070-2_12.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact