Correctly communicating software

Much of the software we use in everyday life consists of distributed components (running on separate cores or even computers) that collaborate through communication (by exchaning messages). It is crucial to develop robust methods that can give reliable guarantees about the behavior of such message-passing software. With a focus on session types as communication protocols and their foundations in logic, this thesis revolves around the following question:

How can we push the boundaries of the logical foundations of session types (binary and multiparty), extending their expressiveness and applicability, while preserving fundamental correctness properties?

In this context, this thesis studies several intertwined aspects of message-passing.

• Network Topology and Asynchronous Communication. Deadlock-freedom is a notoriously hard problem, but session types can be enhanced to restrict component connections to guarantee deadlock-freedom. This thesis studies the effects of asynchronous communication (non-simultaneous sending/receiving) on deadlock-freedom.
• Non-determinism. Non-deterministic choices model how programs may follow different paths of execution (e.g., under external influence). This thesis explores and compares non-deterministic choice constructs with fine-grained semantics, with enhanced session types that maintain the expected correctness properties.
• Ownership. Session types have a foundation in linear logic, a logic with fine-grained resource control in terms of number of uses. This thesis develops an alternative logical foundation and accompanying variant of the pi-calculus based on the logic of bunched implications, similar to linear logic but with a focus on ownership of resources.
• Functions. Thus far, all models of message-passing are concurrent and process-based, but there are also such models for sequential, functional programming. This thesis presents several functional models of message-passing, and guarantees correctness through translation into the process-based models discussed above.
• Multiparty Session Types (MPSTs): Asynchronous and Distributed. MPSTs describe protocols between multiple components; they are practical, but correctness guarantees are complex. This thesis analyzes MPSTs implemented as distributed, asynchronously communicating networks by reduction to the binary session types discussed so far.

Knowing exactly how a program is implemented (as assumed in the topics above) is not always practically feasible. This thesis adapts the approach above to use MPSTs to monitor the behavior of programs with unknown specification, maintaining some correctness guarantees for asynchronous and distributed implementations of MPSTs.