Prioritise the best variation

DOI10.1007/978-3-030-78089-0_6zbMATH Open1490.68141arXiv2103.14466OpenAlexW3177169713MaRDI QIDQ2117016FDOQ2117016

Authors: Wen Kokke, Ornela Dardha 

Publication date: 21 March 2022

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $lambda$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

Full work available at URL: https://arxiv.org/abs/2103.14466

Recommendations

• A new linear logic for deadlock-free session-typed processes
• Comparing deadlock-free session typed processes
• Propositions as sessions
• Comparing type systems for deadlock freedom
• Deadlock and lock freedom in the linear \(\pi\)-calculus

zbMATH Keywords

CPfunctional programming\(\pi\)-calculussession typesdeadlock freedom\( \pi \)-calculusGV

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Linear logic
• Multiparty asynchronous session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Global progress for dynamically interleaved multiparty sessions
• A New Type System for Deadlock-Free Processes
• Type systems for concurrent programs.
• Propositions as sessions
• Deadlock-freedom-by-design, multiparty asynchronous global programming
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Session types as intuitionistic linear propositions
• Linear type theory for asynchronous session types
• A system of interaction and structure
• A new linear logic for deadlock-free session-typed processes
• Proofs as processes
• On the \(\pi\)-calculus and linear logic
• Session types revisited
• Deadlock analysis of unbounded process networks
• Deadlock and lock freedom in the linear \(\pi\)-calculus
• Deadlock analysis of unbounded process networks
• Multiparty Session Types Within a Canonical Binary Theory, and Beyond
• Title not available (Why is that?)
• Type checking a multithreaded functional language with session types
• CONCUR 2004 - Concurrency Theory
• Talking bananas: structural recursion for session types
• Comparing deadlock-free session typed processes
• Choreographies, logically
• Higher-order processes, functions, and sessions: a monadic integration
• Title not available (Why is that?)
• Polarized Substructural Session Types
• A Semantics for Propositions as Sessions
• Prioritise the best variation
• Global types with internal delegation
• Comparing type systems for deadlock freedom
• Types for deadlock-free higher-order programs
• Functions as session-typed processes
• Behavioural analysis of sessions using the calculus of structures
• A graphical approach to progress for structured communication in web services
• Taking linear logic apart
• Title not available (Why is that?)
• Manifest deadlock-freedom for shared session types
• Separating Sessions Smoothly

Cited In (6)

• Prioritise the best variation
• Comparing type systems for deadlock freedom
• Comparing deadlock-free session typed processes
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Asynchronous functional sessions: cyclic and concurrent
• Separating Sessions Smoothly

This page was built for publication: Prioritise the best variation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117016)