Safe session-based concurrency with shared linear state

DOI10.1007/978-3-031-30044-8_16zbMATH Open1541.6809MaRDI QIDQ6535247FDOQ6535247

Authors: Pedro Leite Rocha, Luís Caires 

Publication date: 24 November 2023

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) 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)

Cites Work

• Practical affine types
• From Algol to polymorphic linear lambda-calculus
• Linear logic
• Intuitionistic light affine logic
• Computational interpretations of linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Title not available (Why is that?)
• Hoare type theory, polymorphism and separation
• The \(\pi\)-calculus: A theory of mobile processes
• Title not available (Why is that?)
• Conversation types
• A New Type System for Deadlock-Free Processes
• Logic Programming with Focusing Proofs in Linear Logic
• Title not available (Why is that?)
• Propositions as sessions
• Session types as intuitionistic linear propositions
• Monitors
• Logical Semantics of Types for Concurrency
• Structured Interactional Exceptions in Session Types
• A type system for lock-free processes
• Title not available (Why is that?)
• A new linear logic for deadlock-free session-typed processes
• A concurrent model for linear logic
• Linear logical relations for session-based concurrency
• Proof-carrying code in a session-typed process calculus
• Mobile Processes and Termination
• Linear logical relations and observational equivalences for session-based concurrency
• Propositions as sessions
• Behavioral polymorphism and parametricity in session-based communication
• Termination of processes
• Strong normalisation in the \(\pi\)-calculus
• Typing termination in a higher-order concurrent imperative language
• On the \(\pi\)-calculus and linear logic
• \(L^3\): a linear language with locations
• Structural cut elimination. I: Intuitionistic and classical logic
• Linear logic propositions as session types
• An introduction to differential linear logic: proof-nets, models and antiderivatives
• Talking bananas: structural recursion for session types
• Corecursion and non-divergence in session-typed processes
• Integrating linear and dependent types
• A Hybrid Type System for Lock-Freedom of Mobile Processes
• Linearity, control effects, and behavioral types
• Manifest deadlock-freedom for shared session types
• On polymorphic sessions and functions. A tale of two (fully abstract) encodings
• Conflation confers concurrency
• Affine sessions
• The type discipline of behavioral separation
• Towards races in linear logic
• Resource sharing via capability-based multiparty session types

Cited In (2)

• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Safety of a Client-Based Version Vector Consistency Protocol of Session Guarantees

This page was built for publication: Safe session-based concurrency with shared linear state

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