Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Expressivity of Typed Concurrent Calculi

Joseph William Neal Paulus

TL;DR

This work investigates the expressivity of typed concurrent calculi relative to sequential computation by constructing type-preserving encodings from resource λ-calculi with non-determinism and explicit failure into a session-typed π-calculus. The approach hinges on non-idempotent intersection types for the λ-side and session types linked to linear logic for the π-side, enabling precise, resource-aware translations and correctness proofs. It distinguishes confluent and non-confluent forms of nondeterminism, introduces sharing-based techniques to manage multiple variable occurrences, and extends the framework to unrestricted resources via a second calculi, λ^{!⟂} , with corresponding encodings. Correctness is established through Gorla-style criteria (type preservation, operational completeness and soundness, and success sensitivity) adapted to typed settings, culminating in a two-step encoding chain and several motivating examples. The results illuminate a deep connection between sequential resource-conscious reasoning and concurrent protocol-based interaction, with potential applications in designing typed functional-concurrent languages and reasoning about resource-aware verification. The work thereby advances the understanding of how interactive behavior generalizes sequential computation and provides a robust methodology for transferring reasoning techniques across paradigms.}

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.

On the Expressivity of Typed Concurrent Calculi

TL;DR

This work investigates the expressivity of typed concurrent calculi relative to sequential computation by constructing type-preserving encodings from resource λ-calculi with non-determinism and explicit failure into a session-typed π-calculus. The approach hinges on non-idempotent intersection types for the λ-side and session types linked to linear logic for the π-side, enabling precise, resource-aware translations and correctness proofs. It distinguishes confluent and non-confluent forms of nondeterminism, introduces sharing-based techniques to manage multiple variable occurrences, and extends the framework to unrestricted resources via a second calculi, λ^{!⟂} , with corresponding encodings. Correctness is established through Gorla-style criteria (type preservation, operational completeness and soundness, and success sensitivity) adapted to typed settings, culminating in a two-step encoding chain and several motivating examples. The results illuminate a deep connection between sequential resource-conscious reasoning and concurrent protocol-based interaction, with potential applications in designing typed functional-concurrent languages and reasoning about resource-aware verification. The work thereby advances the understanding of how interactive behavior generalizes sequential computation and provides a robust methodology for transferring reasoning techniques across paradigms.}

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.
Paper Structure (184 sections, 174 theorems, 114 equations, 69 figures, 1 table)

This paper contains 184 sections, 174 theorems, 114 equations, 69 figures, 1 table.

Table of Contents

  1. Introduction
  2. Context and Research Question
  3. Phenomena and Properties
  4. Type Systems
  5. Research Question
  6. Background
  7. Approach
  8. Sequential Models: Resource $\lambda$-Calculi
  9. Non-Determinism and Explicit Failure
  10. Concurrent Models: Session-Typed $\pi$-Calculi
  11. Confluent Non-Determinism
  12. Non-Confluent Non-Determinism
  13. Outline of Contributions
  14. Associated Publications
  15. Non-Deterministic Functions as Non-Deterministic Processes
  16. ...and 169 more sections

Key Result

Proposition 2.2.1

For all $\mathbb{N}$, $\mathbb{N}_1$, $\mathbb{N}_2$ in $\lambda^{\lightning}_{\oplus}\xspace$ s.t. $\mathbb{N} \longrightarrow \mathbb{N}_1$, $\mathbb{N} \longrightarrow \mathbb{N}_2$ with $\mathbb{N}_1 \neq \mathbb{N}_2$ then there exists $\mathbb{M}$ such that $\mathbb{N}_1 \longrightarrow \mathb

Figures (69)

  • Figure 1: Translation of $\lambda$ into $\pi$ as first presented by Milner92
  • Figure 2: Example reduction from Milner92
  • Figure 6: Overview of our approach.
  • Figure 7: Reduction Rules for $\lambda^{\lightning}_{\oplus}\xspace$
  • Figure 8: Typing Rules for $\lambda_{\oplus}$
  • ...and 64 more figures

Theorems & Definitions (180)

  • Proposition 2.2.1: Diamond Property for
  • Remark 2.2.1: A Sub-calculus without Failure ($\lambda_{\oplus}$)
  • Lemma 2.2.1: Linear Substitution Lemma for
  • Theorem 2.1: Subject Reduction for
  • Lemma 2.2.2: Linear Anti-substitution Lemma for
  • Theorem 2.2: Subject Expansion for
  • Lemma 2.2.3: Substitution Lemma for
  • Theorem 2.3: Subject Reduction in
  • Theorem 2.4: Failure of Subject Expansion in
  • Proposition 2.3.1: Diamond Property for $\widehat{\lambda}^{\lightning}_{\oplus}$
  • ...and 170 more