Session types as intuitionistic linear propositions

DOI10.1007/978-3-642-15375-4_16zbMATH Open1287.68125OpenAlexW1607623316MaRDI QIDQ3584932FDOQ3584932

Authors: Luís Caires, Frank Pfenning 

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

Recommendations

• Linear logic propositions as session types
• A linear account of session types in the pi calculus
• A new linear logic for deadlock-free session-typed processes
• Propositions as sessions
• Linearity, session types and the pi calculus

Mathematics Subject Classification ID

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

Cited In (89)

• A formal theory of choreographic programming
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Title not available (Why is that?)
• On the concurrent computational content of intermediate logics
• Functions as session-typed processes
• Nested session types
• I got plenty o' nuttin'
• Relating Functional and Imperative Session Types
• Behavioural analysis of sessions using the calculus of structures
• \textsc{Lincx}: a linear logical framework with first-class contexts
• Causal computational complexity of distributed processes
• Title not available (Why is that?)
• Taking linear logic apart
• Title not available (Why is that?)
• Session-typed concurrent contracts
• Stateful Behavioral Types for Active Objects
• Polymorphic lambda calculus with context-free session types
• A higher-order logic for concurrent termination-preserving refinement
• Session coalgebras: a coalgebraic view on session types and communication protocols
• Linear logic propositions as session types
• Fundamentals of session types
• Propositions as sessions
• On polymorphic sessions and functions. A tale of two (fully abstract) encodings
• An extensible approach to session polymorphism
• Comparing type systems for deadlock freedom
• Relating reasoning methodologies in linear logic and process algebra
• On session types and polynomial time
• Parametrized fixed points and their applications to session types
• Certifying data in multiparty session types
• Cut reduction in linear logic as asynchronous session-typed communication
• On sessions and infinite data
• Conflation confers concurrency
• Linearity, control effects, and behavioral types
• Affine sessions
• A message-passing interpretation of adjoint logic
• A linear account of session types in the pi calculus
• Linearity, session types and the pi calculus
• Title not available (Why is that?)
• Corecursion and non-divergence in session-typed processes
• Modelling session types using contracts
• On asynchronous eventful session semantics
• Observed Communication Semantics for Classical Processes
• Comparing deadlock-free session typed processes
• Combining behavioural types with security analysis
• Fairness and communication-based semantics for session-typed languages
• Linear logical relations and observational equivalences for session-based concurrency
• Multiparty session types, beyond duality
• Type-Based Analysis for Session Inference (Extended Abstract)
• Mixed sessions
• Session types revisited
• On projecting processes into session types
• Verifiable abstractions for contract-oriented systems
• Title not available (Why is that?)
• A Semantics for Propositions as Sessions
• Session Types with Arithmetic Refinements
• Fair subtyping for multi-party session types
• Multiparty session types as coherence proofs
• A core model for choreographic programming
• Choreographies, logically
• Event structure semantics for multiparty sessions
• Proof-carrying code in a session-typed process calculus
• Linear logical relations for session-based concurrency
• Multiparty Session Types Within a Canonical Binary Theory, and Beyond
• Session Types with Gradual Typing
• The true concurrency of differential interaction nets
• Linear resources in Isabelle/HOL
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Title not available (Why is that?)
• Concurrent Process Histories and Resource Transducers
• Safe session-based concurrency with shared linear state
• Substructural proofs as automata
• Binary session types for psi-calculi
• Global types and event structure semantics for asynchronous multiparty sessions
• Circular proofs as session-typed processes: a local validity condition
• Linear \(\lambda \mu\) is CP (more or less)
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Deadlock freedom for asynchronous and cyclic process networks
• Title not available (Why is that?)
• Comparing session type systems derived from linear logic
• Quantum CPOs
• Non-linear communication via graded modal session types
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Asynchronous functional sessions: cyclic and concurrent
• Towards races in linear logic
• A subexponential view of domains in session types
• Non-linearity as the metric completion of linearity
• A universal session type for untyped asynchronous communication
• Resource sharing via capability-based multiparty session types
• Non-blocking concurrent imperative programming with session types

This page was built for publication: Session types as intuitionistic linear propositions

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