Linear logical relations and observational equivalences for session-based concurrency

DOI10.1016/j.ic.2014.08.001zbMath1309.68141OpenAlexW2054150540WikidataQ57652382 ScholiaQ57652382MaRDI QIDQ476190

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Publication date: 28 November 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2014.08.001

zbMATH Keywords

linear logicconfluencestrong normalizationprocess calculisession typeslogical relationsobservational equivalences

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

Characteristic bisimulation for higher-order session processes, Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less), Comparing type systems for deadlock freedom, Fairness and communication-based semantics for session-typed languages, Combining behavioural types with security analysis, Event structure semantics for multiparty sessions, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, POPLMark reloaded: Mechanizing proofs by logical relations, Unnamed Item, Unnamed Item, Unnamed Item, Observed Communication Semantics for Classical Processes, Nested session types, Multiparty Session Types Within a Canonical Binary Theory, and Beyond, Polymorphic lambda calculus with context-free session types

Uses Software

• Lolliproc

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Strong normalisation in the \(\pi\)-calculus
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Confluence for process verification
• Computational interpretations of linear logic
• Towards an algebraic theory of typed mobile processes
• Typing termination in a higher-order concurrent imperative language
• Linearity and bisimulation
• A calculus of mobile processes. II
• On the expressiveness of internal mobility in name-passing calculi
• Soft linear logic and polynomial time
• Genericity and the \(\pi\)-calculus
• Linear Logical Relations for Session-Based Concurrency
• Proof-Carrying Code in a Session-Typed Process Calculus
• Mobile Processes and Termination
• A short survey of isomorphisms of types
• Session Types as Intuitionistic Linear Propositions
• Logical Semantics of Types for Concurrency
• Logical relations and the typed λ-calculus
• On confluence in the π-calculus
• Typed behavioural equivalences for processes in the presence of subtyping
• Propositions as sessions
• Lolliproc
• Behavioral Polymorphism and Parametricity in Session-Based Communication
• Termination of processes
• Behavioral equivalence in the polymorphic pi-calculus
• Intensional interpretations of functionals of finite type I