License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.Gabbrielli.3
URN: urn:nbn:de:0030-drops-132256
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13225/
Go to the corresponding OASIcs Volume Portal

Dezani-Ciancaglini, Mariangiola ; Giannini, Paola ; Venneri, Betti

Deconfined Intersection Types in Java

pdf-format:
OASIcs-Gabbrielli-3.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{dezaniciancaglini_et_al:OASIcs:2020:13225,
  author =	{Mariangiola Dezani-Ciancaglini and Paola Giannini and Betti Venneri},
  title =	{{Deconfined Intersection Types in Java}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{3:1--3:25},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{Frank S. de Boer and Jacopo Mauro},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13225},
  URN =		{urn:nbn:de:0030-drops-132256},
  doi =		{10.4230/OASIcs.Gabbrielli.3},
  annote =	{Keywords: Intersection Types, Featherweight Java, Lambda Expressions}
}

Keywords: Intersection Types, Featherweight Java, Lambda Expressions
Collection: Recent Developments in the Design and Implementation of Programming Languages
Issue Date: 2020
Date of publication: 27.11.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI