TY - GEN
T1 - Deconfined intersection types in java
AU - Dezani-Ciancaglini, Mariangiola
AU - Giannini, Paola
AU - Venneri, Betti
N1 - Publisher Copyright:
© Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri; licensed under Creative Commons License CC-BY
PY - 2020/11/1
Y1 - 2020/11/1
N2 - 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.
AB - 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.
KW - Featherweight Java
KW - Intersection Types
KW - Lambda Expressions
UR - https://www.scopus.com/pages/publications/85115851393
U2 - 10.4230/OASIcs.Gabbrielli.2020.3
DO - 10.4230/OASIcs.Gabbrielli.2020.3
M3 - Conference contribution
AN - SCOPUS:85115851393
T3 - OpenAccess Series in Informatics
BT - Recent Developments in the Design and Implementation of Programming Languages - Gabbrielli's Festschrift
A2 - de Boer, Frank S.
A2 - Mauro, Jacopo
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 2020 Recent Developments in the Design and Implementation of Programming Languages - Gabbrielli's Festschrift
Y2 - 27 November 2020
ER -