## My work

Research interests: nominal calculi, concurrency, category theory, algebras and coalgebras, temporal and spatial logics for nominal calculi, automata and languages with names, quantitative reasoning, c-semirings, service-oriented computing and formal methods for system design. Recent work: presheaf categories and nominal sets, and their algorithmic counterpart: named sets and history-dependent automata.

## My publications

(direct link to the bibtex file)

## Ph.D. Thesis

My thesis is called "Accessible functors and final coalgebras for named sets" and has been reviewed by Dr. Marcelo Fiore and Dr. Alexander Kurz.

### Abstract

In the field of programming language semantics and concurrency theory, wide attention is paid to the so called \emph{name-passing calculi}, i.e. formalisms where name generation and passing play a fundamental role. A prototypical example is provided by the $\pi$-calculus. The peculiarities of name passing required to refine existing theoretical models and to invent new ones, such as coalgebras over \emph{presheaf} categories. The theory of name passing has proven difficult to be used in applications, since many problems arise due to the presence of fresh names. For example, only a few specialised tools exist for automated verification of nominal calculi, such as the \emph{mobility workbench} or \emph{mihda}, the latter exploiting a model of computation with \emph{local} names, called \emph{history-dependent automata}, defined as coalgebras in the category of \emph{named sets}. History dependent automata have been successful in modelling a certain number of formalisms with name passing. However, there has always been a gap between the definitions on presheaf categories, exploiting mathematical tools such as accessible functors, and definitions of coalgebras on named sets, that are given for each language in an ad-hoc way, often tied to implementation purposes. In this thesis work we try to fill this gap, by linking history-dependent automata with the theoretical results that ensure correctness and full abstractness of the semantics of calculi in presheaf categories. In particular, we define a meta-language of \emph{accessible} endofunctors in the category of named sets, that can be used to define the semantics of calculi in a modular way. We show how locality of names is reflected in mathematical properties of the functors, in a way that is close to intuition and common practice related to local names themselves. We also provide a coalgebraic characterisation of the semantics of the $\pi$-calculus as a finitely branching system, making sense in the general case of a representation technique that was used in previous work by Ferrari, Montanari and Tuosto (TCS 2005) to minimise finite-state $\pi$-calculus agents, and of the causal semantics of Petri nets that was presented in previous work by Montanari aand Pistore (STACS 1997).