Tipi globali per reti asincrone: un approccio coinduttivo

Abstract

I tipi globali sono un semplice, ma espressivo formalismo di tipo, usato per modellare la struttura delle interazioni desiderate tra più partecipanti che si scambiano messaggi in una rete. Tradizionalmente i tipi globali sono stati usati per assicurare proprietà di sicurezza delle interazioni, come per esempio l'assenza di errori di comunicazione, l'assenza di deadlock e di corse critiche. Usando la nozione di proiezione è possibile ottenere tipi locali per i partecipanti, che rappresentano il comportamento atteso. In questo modo è possibile verificare che la rete si evolverà come descritto nel tipo globale. Nella tesi abbiamo sviluppato un'implementazione, usando il paradigma di co-logic programming, di una nuova proposta di tipi globali per reti asincrone, in cui l'asincronia è espressa al livello del type system. Oltre a fornire una versione eseguibile del typechecking, il beneficio di questa implementazione è di forzare a capire ed esprimere chiaramente la natura o induttiva o coinduttiva delle definizioni e i relativi problemi di terminazione.

Global types are a simple but expressive type formalism, used to model the intended interaction structure among multiple participants exchanging messages in a network. Traditionally, global types have been used to ensure safety properties of interactions, such as absence of communication errors, deadlock freedom and race freedom. Using the notion of projection it is possible to obtain local types for the participants, which represent their expected behaviour. In this way, it is possible to check that the network will evolve as defined in the global type. In the thesis, we have developed an implementation in co-logic programming of a novel formulation of global types for asynchronous networks, where asynchrony is expressed at the level of the type system. Besides providing an executable version of typechecking, the benefit of this encoding is that it forces to clearly understand and express the either inductive or coinductive nature of definitions, and the related termination issues.