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.

Accessible functors and final coalgebras for named sets.

CIANCIA, VINCENZO
2008

Abstract

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.
15-nov-2008
Italiano
alpha-conversion
coalgebras
functors
garbage collection
Named sets
nominal calculi
nominal sets
Montanari, Ugo
File in questo prodotto:
File Dimensione Formato  
tesi.pdf

embargo fino al 15/12/2048

Tipologia: Altro materiale allegato
Dimensione 707.05 kB
Formato Adobe PDF
707.05 kB Adobe PDF

I documenti in UNITESI sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.14242/148489
Il codice NBN di questa tesi è URN:NBN:IT:UNIPI-148489