Resource-awareness for Java-like languages and beyond

Reasoning about programs and their correctness concerns, in the first place, their input/output behaviour. However, there are many important properties which are non-extensional, that is, allow to further classify programs. Among those, a significant class are the properties related to the resources needed to carry out the computation successfully. There are many possible views of what a "resource" is, e.g., space or time complexity; in this thesis, a resource is meant to be some external data, used in a program through an internal name (a variable), and resource-awareness means the ability to track, statically and/or at runtime, how these resources are used by the program. The aim of this thesis is to provide design guidelines and formal foundations to smoothly add resource-awareness to a programming language, mainly focusing on the object-oriented paradigm. This is a novelty, since in the literature resource-awareness has been studied in the context of functional languages. To achieve this goal, the key idea is to use annotations, called grades, which, intuitively, represent the availability of a resource. These annotations are elements of an algebraic structure called grade algebra, and both type system and reduction are given parametrically on an arbitrary grade algebra, modeling a particular kind of usages. We also investigate the possibility for to the programmer to define her/his grades. The thesis includes two chapters which achieve additional results, notably the application of the proposed approach to a functional language, a novel formulation of resource-aware semantics, and an application of grades to a challenging case, that is, to characterize sharing and immutability properties in the context of imperative languages.