On the Expressivity of Typed Concurrent Calculi

This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. We focus 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, this thesis addresses the following research question: how exactly does interactive behavior generalize sequential computation? We seek 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’, our approach contrasts these two fundamental computational models via correct translations, which formally explain how sequential terms in λ can be codified into concurrent processes in π. The main novelty is the use of behavioral 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 our translations.

We delve into our research question along several dimensions. First, we consider non-deterministic computations, whereby reductions may have branching behaviors. 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, we also consider 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 π) we provide an original connection between these two important and widely-studied type disciplines along the dimensions of interest. Finally, we contrast 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.