On the expressivity of typed concurrent calculi

This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. The focus lies on programming calculi, both functional (sequential) and concurrent, as they provide a compelling rigorous framework for evaluating program semantics and for developing analyses and program verification techniques.

More concretely, Joe Paulus addresses the following research question: how exactly does interactive behaviour generalise sequential computation? Paulus seeks to gauge the expressivity of the π-calculus—the paradigmatic calculus of concurrency and interaction—with respect to sequential computation as captured by the λ-calculus. Building upon Milner’s seminal work on ‘functions as processes’, his approach contrasts these two fundamental computational models via correct translations, which formally explain how sequential terms in λ can be codified into concurrent processes in π. Paulus' main novelty is the use of behavioural types, advanced type systems for terms (in λ) and processes (in π), to define the calculi, establish the properties of typed terms/processes, and to prove the correctness of his translations.

Paulus studied his research question via several dimensions. First, he considered non-deterministic computations, whereby reductions may have branching behaviours. Non-determinism brings flexibility and generality in specifications; it may be confluent or non-confluent: in the former case, reductions may be independent taken within alternative branches, in a non-committal way; in the latter case committing to one branch discards other alternatives. As another dimension, he also considered resource-aware computation whereby resources are linear (usable exactly once) or unrestricted (usable zero or many times). In turn, resource-awareness paves the way to a principled, explicit treatment of failures in computations, which may occur when there is a lack or excess of resources or when they are misused.

One key insight is that intersection types in the λ-calculus can precisely specify quantitative information of a term as it evolves through computation. By providing tight, type-preserving translations between intersection types (in λ) and session types (in π) Paulus provides an original connection between these two important and widely-studied type disciplines along the dimensions of interest. Finally, he contrasts models of sequential and concurrent computation by considering type systems for concurrency that guarantee termination (strong normalization): this is a well studied and fundamental property for sequential computation models, which is actively studied in the concurrent setting.

Dissertation: https://hdl.handle.net/11370/41054198-864c-44d9-ab7c-8ac8c3c91137