Session Types as Intuitionistic Linear Propositions

DOI10.1007/978-3-642-15375-4_16zbMath1287.68125OpenAlexW1607623316MaRDI QIDQ3584932

Publication date: 31 August 2010

Published in: CONCUR 2010 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15375-4_16

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

Multiparty session types as coherence proofs, On projecting processes into session types, Concurrent Process Histories and Resource Transducers, Relating Functional and Imperative Session Types, Parametrized fixed points and their applications to session types, Behavioural Analysis of Sessions Using the Calculus of Structures, Substructural Proofs as Automata, Non-linearity as the Metric Completion of Linearity, Multiparty session types, beyond duality, Conflation Confers Concurrency, I Got Plenty o’ Nuttin’, Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less), Certifying Data in Multiparty Session Types, Verifiable abstractions for contract-oriented systems, Session types revisited, The true concurrency of differential interaction nets, Comparing type systems for deadlock freedom, Fairness and communication-based semantics for session-typed languages, Combining behavioural types with security analysis, ElixirST: a session-based type system for elixir modules, Non-Deterministic Functions as Non-Deterministic Processes (Extended Version), Stateful Behavioral Types for Active Objects, Event structure semantics for multiparty sessions, Separating Sessions Smoothly, Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic, A formal theory of choreographic programming, Unnamed Item, Choreographies, logically, Unnamed Item, On session types and polynomial time, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Observed Communication Semantics for Classical Processes, Linearity, Control Effects, and Behavioral Types, LINCX: A Linear Logical Framework with First-Class Contexts, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, Unnamed Item, Linear logical relations and observational equivalences for session-based concurrency, Nested session types, On the concurrent computational content of intermediate logics, A core model for choreographic programming, On asynchronous eventful session semantics, Linear logic propositions as session types, Fair subtyping for multi-party session types, An extensible approach to session polymorphism, Modelling session types using contracts, Relating reasoning methodologies in linear logic and process algebra, Fundamentals of session types, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, A message-passing interpretation of adjoint logic, Session Types with Gradual Typing, Corecursion and Non-divergence in Session-Typed Processes, Mixed sessions, Session-typed concurrent contracts, Session Types with Arithmetic Refinements, Multiparty Session Types Within a Canonical Binary Theory, and Beyond, Type-Based Analysis for Session Inference (Extended Abstract), Proof-Carrying Code in a Session-Typed Process Calculus, Unnamed Item, Session typing and asynchronous subtyping for the higher-order $\pi$-calculus, Polymorphic lambda calculus with context-free session types, Causal computational complexity of distributed processes, Prioritise the best variation