Riassunto analitico
In the field of programming language semantics and concurrency theory,
wide attention is paid to the so called 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
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
mobility workbench or mihda, the latter exploiting a model of
computation with local names, called history-dependent automata,
defined as coalgebras in the category of 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
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 had been previously used by Montanari, Ferrari and
Tuosto to minimise finite-state pi-calculus agents.
|
