On the Undecidability of Asynchronous Session Subtyping

DOI10.1007/978-3-662-54458-7_26zbMath1486.68114OpenAlexW2610085676MaRDI QIDQ2988385

Nobuko Yoshida, Julien Lange

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10044/1/44467

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Automata and formal grammars in connection with logical questions (03D05) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (16)

Deconfined Global Types for Asynchronous Sessions ⋮ Precise Subtyping for Asynchronous Multiparty Sessions ⋮ Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types ⋮ Undecidability of asynchronous session subtyping ⋮ Unnamed Item ⋮ Precise subtyping for synchronous multiparty sessions ⋮ A formal theory of choreographic programming ⋮ Partially Typed Multiparty Sessions ⋮ On the boundary between decidability and undecidability of asynchronous session subtyping ⋮ A Sound Algorithm for Asynchronous Session Subtyping ⋮ Fair refinement for asynchronous session types ⋮ Process calculi as a tool for studying coordination, contracts and session types ⋮ Composition and decomposition of multiparty sessions ⋮ Connecting open systems of communicating finite state machines ⋮ Session Types with Arithmetic Refinements ⋮ Input urgent semantics for asynchronous timed session types

Cites Work

• Unnamed Item
• Unnamed Item
• Verifying identical communicating processes is undecidable
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Undecidability of asynchronous session subtyping
• Verification of programs with half-duplex communication
• Subtyping for session types in the pi calculus
• From Communicating Machines to Graphical Choreographies
• Multiparty Session Types Meet Communicating Automata
• Honesty by Typing
• Full Abstraction in a Subtyped pi-Calculus with Linear Types
• Subtyping Supports Safe Session Substitution
• Buffered Communication Analysis in Distributed Multiparty Sessions
• Global Principal Typing in Partially Commutative Asynchronous Sessions
• Session-Based Communication Optimisation for Higher-Order Mobile Processes
• On Communicating Finite-State Machines
• On the progress of communication between two finite state machines
• Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
• Meeting Deadlines Together
• Structured Communication-Centred Programming for Web Services

This page was built for publication: On the Undecidability of Asynchronous Session Subtyping