Safe session-based concurrency with shared linear state

DOI10.1007/978-3-031-30044-8_16MaRDI QIDQ6535247zbMATH OpenFDO

Authors Pedro Leite Rocha, Luís Caires

Publication date 24 November 2023

Copyright license Creative Commons Attribution 4.0 International

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

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

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)