On the Expressivity of Typed Concurrent Calculi

TL;DR

This thesis investigates the expressive power of typed concurrent calculi, providing a detailed analysis of their capabilities in modeling programming languages and aiding in program verification.

Contribution

It offers a comprehensive examination of typed concurrent calculi, highlighting their role in formal semantics and verification methods for programming languages.

Findings

Analyzes the expressivity of typed concurrent calculi.

Provides insights into their application in program semantics.

Enhances understanding of formal models for programming languages.

Abstract

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. This is the full version of the thesis containing appendices.