TY - JOUR
T1 - A Java-like Calculus with User-Defined Coeffects
AU - Bianchini, Riccardo
AU - Dagnino, Francesco
AU - Giannini, Paola
AU - Zucca, Elena
N1 - Publisher Copyright:
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
PY - 2022
Y1 - 2022
N2 - We propose a Java-like calculus where declared variables can be annotated by coeffects specifying constraints on their use, such as linearity or privacy levels. Annotations are written in the language itself, as expressions of type Coeffect, a predefined class which can be extended by user-defined subclasses, modeling the coeffects desired for a specific application. We formalize the type system and prove subject reduction, which includes preservation of coeffects, and show several examples.
AB - We propose a Java-like calculus where declared variables can be annotated by coeffects specifying constraints on their use, such as linearity or privacy levels. Annotations are written in the language itself, as expressions of type Coeffect, a predefined class which can be extended by user-defined subclasses, modeling the coeffects desired for a specific application. We formalize the type system and prove subject reduction, which includes preservation of coeffects, and show several examples.
KW - Java-like languages
KW - operational semantics
KW - type systems
UR - http://www.scopus.com/inward/record.url?scp=85143251551&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:85143251551
SN - 1613-0073
VL - 3284
SP - 66
EP - 78
JO - CEUR Workshop Proceedings
JF - CEUR Workshop Proceedings
T2 - 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022
Y2 - 7 September 2022 through 9 September 2022
ER -