Typed Non-determinism in Concurrent Calculi: The Eager Way
Abstract
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 {\pi}-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 {\pi}-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 {\lambda}-calculus.
Keywords
Cite
@article{arxiv.2411.07714,
title = {Typed Non-determinism in Concurrent Calculi: The Eager Way},
author = {Bas van den Heuvel and Daniele Nantes-Sobrinho and Joseph W. N. Paulus and Jorge A. Pérez},
journal= {arXiv preprint arXiv:2411.07714},
year = {2024}
}
Comments
arXiv admin note: substantial text overlap with arXiv:2408.07915