TY - GEN
T1 - Multi-Graded Featherweight Java
AU - Bianchini, Riccardo
AU - Dagnino, Francesco
AU - Giannini, Paola
AU - Zucca, Elena
N1 - Publisher Copyright:
© Riccardo Bianchini Francesco Dagnino Paola Giannini and Elena Zucca;
PY - 2023/7
Y1 - 2023/7
N2 - 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.
AB - 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.
KW - Graded modal types
KW - Java
UR - http://www.scopus.com/inward/record.url?scp=85165633701&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.ECOOP.2023.3
DO - 10.4230/LIPIcs.ECOOP.2023.3
M3 - Conference contribution
AN - SCOPUS:85165633701
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 37th European Conference on Object-Oriented Programming, ECOOP 2023
A2 - Ali, Karim
A2 - Salvaneschi, Guido
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 37th European Conference on Object-Oriented Programming, ECOOP 2023
Y2 - 17 July 2023 through 21 July 2023
ER -