Bas van den Heuvel ; Daniele Nantes-Sobrinho ; Joseph W. N. Paulus ; Jorge A. Pérez - Typed Non-determinism in Concurrent Calculi: The Eager Way

entics:14735 - Electronic Notes in Theoretical Informatics and Computer Science, December 11, 2024, Volume 4 - Proceedings of MFPS XL - https://doi.org/10.46298/entics.14735
Typed Non-determinism in Concurrent Calculi: The Eager WayArticle

Authors: Bas van den Heuvel ; Daniele Nantes-Sobrinho ; Joseph W. N. Paulus ; Jorge A. Pérez

    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.


    Volume: Volume 4 - Proceedings of MFPS XL
    Published on: December 11, 2024
    Accepted on: November 13, 2024
    Submitted on: November 13, 2024
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 21 times.
    This article's PDF has been downloaded 10 times.