Publications

Conference papers

Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Resource-Aware Soundness for Big-Step Semantics. Proc. ACM Program. Lang., 7(OOPSLA2) :1281–1309, 2023.

Abstract

We extend the semantics and type system of a lambda calculus equipped with common constructs to be resource-aware. That is, reduction is instrumented to keep track of the usage of resources, and the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no needed resource gets exhausted. The resource-aware extension is parametric on an arbitrary grade algebra, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Multi-Graded Featherweight Java. In: Ali, K. and Salvaneschi, G. (eds.) 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, pp. 3:1–3:27, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 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.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto. Coeffects for sharing and mutation. Proc. ACM Program. Lang., 6(OOPSLA2) :870–898, 2022.

Abstract

In type-and-coeffect systems, contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bottom-up, combining, for each term, the coeffects of its subterms, through a fixed set of algebraic operators. We show that this principled approach can be adopted to track sharing in the imperative paradigm, that is, links among variables possibly introduced by the execution. This provides a significant example of non-structural coeffects, which cannot be computed by-variable, since the way a given variable is used can affect the coeffects of other variables. To illustrate the effectiveness of the approach, we enhance the type system tracking sharing to model a sophisticated set of features related to uniqueness and immutability. Thanks to the coeffect-based approach, we can express such features in a simple way and prove related properties with standard techniques.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. A Java-Like Calculus with User-Defined Coeffects. In: Lago, U.D. and Gorla, D. (eds.) Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022, pp. 66–78, CEUR-WS.org, 2022.

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.
Riccardo Bianchini and Francesco Dagnino. Asynchronous Global Types in Co-logic Programming. In: Damiani, F. and Dardha, O. (eds.) Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, pp. 134–146, Springer, 2021.

Abstract

Global types are at the core of communication based programming. They allow a high level specification of protocols involving many participants and enforce good safety and liveness properties, such as absence of deadlock, locked participants and orphan messages. In this paper, we describe an implementation of a novel formalism of global types for sessions with asynchronous communications in co-logic programming, where we use coinduction to properly handle the coinductive syntax of global types and processes. We also define a simple query language to write sessions and global types, providing primitives for type checking.

Journal papers

Riccardo Bianchini and Francesco Dagnino. QueryAGT: Asynchronous global types in co-logic programming. Sci. Comput. Program., 225 :102895, 2023.

Abstract

Global types are at the core of communication-based programming. They allow a high-level specification of protocols involving many participants and enforce good safety and liveness properties, such as deadlock freedom, and the absence of locked participants and orphan messages. The present software provides an implementation in co-logic programming of a novel formalism of global types for sessions with asynchronous communications, where we use coinduction to properly handle the coinductive syntax of global types and processes. It also offers a simple query language to write sessions and global types, providing primitives for type checking.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. A Java-like calculus with heterogeneous coeffects. Theor. Comput. Sci., 971 :114063, 2023.

Abstract

We propose a Java-like calculus where declared variables can be annotated by coeffects specifying constraints on their use, e.g., affinity or privacy levels. Such coeffects are heterogeneous, in the sense that different kinds of coeffects can be used in the same program; combining coeffects of different kinds leads to the trivial coeffect. We prove subject reduction, which includes preservation of coeffects, and show several examples. In a Java-like language, coeffects can be expressed in the language itself, as expressions of user-defined classes.

Workshop papers

Riccardo Bianchini. Monitoring for Resource-Awareness. In: Ancona, D. and Audrito, G. (eds.) Proceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution, VORTEX 2023, Seattle, WA, USA, 18 July 2023, pp. 13–16, ACM, 2023.

Preprint papers

Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Don’t exhaust, don’t waste, https://arxiv.org/abs/2507.13792, 2025.

Abstract

We extend the semantics and type system of a lambda calculus equipped with common constructs to be resource-aware. That is, the semantics keep tracks of the usage of resources, and is stuck, besides in case of type errors, if either a needed resource is exhausted, or a provided resource would be wasted. In such way, the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no resource gets either exhausted or wasted. The no-waste extension is parametric on an arbitrary grade algebra, modeling an arbitrary assortment of possible usages, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, and Elena Zucca. Multi-graded Featherweight Java. CoRR, abs/2302.07782 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.
Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca, and Marco Servetto. Coeffects for Sharing and Mutation. CoRR, abs/2209.07439 2022.

Abstract

In type-and-coeffect systems, contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bottom-up, combining, for each term, the coeffects of its subterms, through a fixed set of algebraic operators. We show that this principled approach can be adopted to track sharing in the imperative paradigm, that is, links among variables possibly introduced by the execution. This provides a significant example of non-structural coeffects, which cannot be computed by-variable, since the way a given variable is used can affect the coeffects of other variables. To illustrate the effectiveness of the approach, we enhance the type system tracking sharing to model a sophisticated set of features related to uniqueness and immutability. Thanks to the coeffect-based approach, we can express such features in a simple way and prove related properties with standard techniques.

PhD thesis

Resource-awareness for Java-like languages and beyond
supervised by Elena Zucca (Unige), Francesco Dagnino (Unige) and Paola Giannini (UniUpo)
DIBRIS - Università di Genova
PhD Program in Computer Science and System Engineering, Cycle XXXVI
Thesis defended in April 23, 2024

Software

Query AGT: An implementation in co-logic programming of the asynchronous global type system with a simple query language to interact with it