Research Profile

Software is pervasive in our lives, and there is virtually no aspect of our society where software does not play a key role. This makes reasoning about software systems, predicting their behaviour, and ensuring their safety and reliability crucial tasks for the sustainability of our digital ecosystem. Programming language semantics, my main field of research, studies the formal meaning of programs and, as such, it plays a crucial role in the aforementioned scenario.

Historically, program semantics has its roots in formal logic and moves from the assumption that, in their bare essence, programs are syntactic objects (code) whose meaning is given by the mathematical entities they denote (such as functions or numbers). Consequently, understanding a program means understanding its denotation. This perspective has been remarkably successful in the past decades, but it can hardly cope with the new challenges of nowadays software systems, such as privacy, security, and environmental impact.

To face them, in my research, I follow a different perspective on program semantics, whereby rather than focusing on their denotations, programs – viewed as bare syntax – are regarded as mathematical objects themselves, exactly as numbers, shapes, and figures. Contrary to the latter (that already come with well-developed mathematics, namely arithmetic, topology, and geometry), however, we still lack a comprehensive mathematics of programs, so that many of the notions that would naturally define the meaning of a program – such as equations, operations, and transformations between programs – are not yet fully understood.

The prime goal of my research is to contribute to the development of a general and effective mathematics of programs. To do so, I depart from traditional mathematics taking, instead, a relational point of view: I am firmly convinced that if we want to achieve a solid understanding of programs, we should not focus on programs as isolated objects, but on the way programs relate to one another, and thus on relations between them. Following this perspective, I work on the development of a mathematical theory of program relations, namely an algebra and calculus where program relations with their operations and laws are first-class citizens, and apply such a theory to re-build program semantics on a relational basis.