DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2023.3

Multi-Graded Featherweight Java

Authors: Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract

Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a variable is needed. We extend the type system of Featherweight Java to be resource-aware, parametrically on an arbitrary grade algebra modeling a specific usage of resources. We prove that this type system is sound with respect to a resource-aware version of reduction, that is, a well-typed program has a reduction sequence which does not get stuck due to resource consumption. Moreover, we show that the available grades can be heterogeneous, that is, obtained by combining grades of different kinds, via a minimal collection of homomorphisms from one kind to another. Finally, we show how grade algebras and homomorphisms can be specified as Java classes, so that grade annotations in types can be written in the language itself.

Cite as

Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Multi-Graded Featherweight Java. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 3:1-3:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bianchini_et_al:LIPIcs.ECOOP.2023.3,
  author =	{Bianchini, Riccardo and Dagnino, Francesco and Giannini, Paola and Zucca, Elena},
  title =	{{Multi-Graded Featherweight Java}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{3:1--3:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.3},
  URN =		{urn:nbn:de:0030-drops-181960},
  doi =		{10.4230/LIPIcs.ECOOP.2023.3},
  annote =	{Keywords: Graded modal types, Java}
}

Search Results

Documents authored by Bianchini, Riccardo

Multi-Graded Featherweight Java

Abstract

Cite as

Thanks for your feedback!

Could not send message