Typed Non-determinism in Concurrent Calculi: The Eager Way
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916527891021824 |
|---|---|
| author | Heuvel, Bas van den Nantes-Sobrinho, Daniele Paulus, Joseph W. N. Pérez, Jorge A. |
| author_facet | Heuvel, Bas van den Nantes-Sobrinho, Daniele Paulus, Joseph W. N. Pérez, Jorge A. |
| contents | We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is constrained by the delicate tension between non-determinism and linearity. Prior work developed a session-typed π-calculus with standard non-deterministic choice; well-typed processes enjoy type preservation and deadlock-freedom. Central to this typed calculus is a lazy semantics that gradually discards branches in choices. This lazy semantics, however, is complex: various technical elements are needed to describe the non-deterministic behavior of typed processes. This paper develops an entirely new approach, based on an eager semantics, which more directly represents choices and commitment. We present a π-calculus in which non-deterministic choices are governed by this eager semantics and session types. We establish its key correctness properties, including deadlock-freedom, and demonstrate its expressivity by correctly translating a typed resource λ-calculus. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_07714 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Typed Non-determinism in Concurrent Calculi: The Eager Way Heuvel, Bas van den Nantes-Sobrinho, Daniele Paulus, Joseph W. N. Pérez, Jorge A. Logic in Computer Science Programming Languages We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is constrained by the delicate tension between non-determinism and linearity. Prior work developed a session-typed π-calculus with standard non-deterministic choice; well-typed processes enjoy type preservation and deadlock-freedom. Central to this typed calculus is a lazy semantics that gradually discards branches in choices. This lazy semantics, however, is complex: various technical elements are needed to describe the non-deterministic behavior of typed processes. This paper develops an entirely new approach, based on an eager semantics, which more directly represents choices and commitment. We present a π-calculus in which non-deterministic choices are governed by this eager semantics and session types. We establish its key correctness properties, including deadlock-freedom, and demonstrate its expressivity by correctly translating a typed resource λ-calculus. |
| title | Typed Non-determinism in Concurrent Calculi: The Eager Way |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2411.07714 |