Bisimulation theory is a co-inductive tool used as a tractable method for studying equivalence
relations in process calculi. This dissertation studies bisimulation theory for session types. We
define the Asynchronous Session π-calculus (ASP for short), which is a session type calculus
with queue configurations acting as a communication medium at each session endpoint The
semantics for ASP offer fine-grained communication that enjoys the non-blocking property
of asynchrony and the order-preserving property of session types. The ASP typing system is
shown to be sound to guarantee type safety in the presence of subtyping. A typed labelled
transition system gives rise to a bisimilarity which is sound and complete with respect to typed
reduction-closed congruence. The bisimilarity theory of ASP highlights the determinacy and
confluence properties of session types.
Event-driven programming is one of the major paradigms that utilise the asynchronous nature
of distributed systems, where events are recognised as the presence of messages and their
typed information in the communication medium. To justify the design choices made, we
develop a superset of ASP, called the Eventful Session π-calculus (ESP for short), equipped
with the minimal session primitives for an expressive event-driven computational model. The
eventful session type system introduces the session set type, which is a collection of session
types used to type a set of possible events. The ESP typing system maintains its consistency
with respect to the ASP session typing system up-to a subtyping relation for session set types.
The straightforward extension from ASP to ESP offers behavioural transparency, making the
bisimilarity theory for the ASP a special case for the ESP theory – the bisimilarity relation
coincides with typed reduction-closed congruence and determinacy and confluence properties
are shown to hold for session transitions.
Many studies regarding event-driven computation have identified the selector or its equivalent,
the polling operator, as the key construct for describing an event-driven framework. The
selector is defined as a higher level construct in ESP and it is used to implement the core event
handling routine called the event loop. Following the empirical study by Lauer and Needham,
we define a session-based transformation from a multi-threaded server to an event loop server.
Confluence theory proves that the transformation is type- and semantics-preserving.
In the last part of the dissertation we extend the behavioural theory to multiparty session
types, both in the synchronous and the asynchronous cases. For each case, we examine two
different typed labelled transition systems. In the first case we examine a standard labelled
transition system with respect to the local session typing of processes. In the second case
a choreography specification governs the behaviour of a multiparty session process and its
observer. Each labelled transition system defines a bisimilarity relation, which coincides with
the corresponding reduction-closed congruence.