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

Dipartimento per lo Sviluppo Sostenibile e la Transizione Ecologica

Risultato della ricerca: Contributo su rivista › Articolo da conferenza › 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.

Lingua originale	Inglese
pagine (da-a)	66-78
Numero di pagine	13
Rivista	CEUR Workshop Proceedings
Volume	3284
Stato di pubblicazione	Pubblicato - 2022
Evento	23rd Italian Conference on Theoretical Computer Science, ICTCS 2022 - Rome, Italy Durata: 7 set 2022 → 9 set 2022

Altri file e collegamenti

Link to publication in Scopus

Cita questo

@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

Altri file e collegamenti

Fingerprint

Cita questo