A Java-like Calculus with User-Defined Coeffects

Riccardo Bianchini; Francesco Dagnino; Paola Giannini; Elena Zucca

A Java-like Calculus with User-Defined Coeffects

Riccardo Bianchini
, Francesco Dagnino
, Paola Giannini
, Elena Zucca

Department of Sustainable Development and Ecological Transition

Research output: Contribution to journal › Conference article › peer-review

Abstract

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.

Original language	English
Pages (from-to)	66-78
Number of pages	13
Journal	CEUR Workshop Proceedings
Volume	3284
Publication status	Published - 2022
Event	23rd Italian Conference on Theoretical Computer Science, ICTCS 2022 - Rome, Italy Duration: 7 Sept 2022 → 9 Sept 2022

Keywords

Java-like languages
operational semantics
type systems

Cite this

@article{9f74795afc8f4bb58fda10259a7fb457,

title = "A Java-like Calculus with User-Defined Coeffects",

abstract = "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.",

keywords = "Java-like languages, operational semantics, type systems",

author = "Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca",

note = "Publisher Copyright: {\textcopyright} 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).; 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022 ; Conference date: 07-09-2022 Through 09-09-2022",

year = "2022",

language = "English",

volume = "3284",

pages = "66--78",

journal = "CEUR Workshop Proceedings",

issn = "1613-0073",

publisher = "CEUR-WS",

}

TY - JOUR

T1 - A Java-like Calculus with User-Defined Coeffects

AU - Bianchini, Riccardo

AU - Dagnino, Francesco

AU - Giannini, Paola

AU - Zucca, Elena

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 - https://www.scopus.com/pages/publications/85143251551

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 -

A Java-like Calculus with User-Defined Coeffects

Abstract

Keywords

Other files and links

Fingerprint

Cite this