Session types as intuitionistic linear propositions

DOI10.1007/978-3-642-15375-4_16MaRDI QIDQ3584932zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(89)

• Linear resources in Isabelle/HOL
• A formal theory of choreographic programming
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• scientific article; zbMATH DE number 7441269 (Why is no real title available?)
• On the concurrent computational content of intermediate logics
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Functions as session-typed processes
• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• Nested session types
• I got plenty o' nuttin'
• 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
• Relating Functional and Imperative Session Types
• scientific article; zbMATH DE number 7649947 (Why is no real title available?)
• Taking linear logic apart
• scientific article; zbMATH DE number 6131659 (Why is no real title available?)
• Session-typed concurrent contracts
• 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
• Stateful Behavioral Types for Active Objects
• Fundamentals of session types
• Linear logic propositions as session types
• Propositions as sessions
• On polymorphic sessions and functions. A tale of two (fully abstract) encodings
• Comparing type systems for deadlock freedom
• On session types and polynomial time
• An extensible approach to session polymorphism
• Parametrized fixed points and their applications to session types
• Relating reasoning methodologies in linear logic and process algebra
• Concurrent Process Histories and Resource Transducers
• Certifying data in multiparty session types
• Conflation confers concurrency
• Cut reduction in linear logic as asynchronous session-typed communication
• Linearity, control effects, and behavioral types
• On sessions and infinite data
• Substructural proofs as automata
• Binary session types for psi-calculi
• Safe session-based concurrency with shared linear state
• A message-passing interpretation of adjoint logic
• Affine sessions
• A linear account of session types in the pi calculus
• Linear \(\lambda \mu\) is CP (more or less)
• Circular proofs as session-typed processes: a local validity condition
• Global types and event structure semantics for asynchronous multiparty sessions
• Linearity, session types and the pi calculus
• Corecursion and non-divergence in session-typed processes
• scientific article; zbMATH DE number 7471698 (Why is no real title available?)
• 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
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Deadlock freedom for asynchronous and cyclic process networks
• Multiparty session types, beyond duality
• Mixed sessions
• Type-Based Analysis for Session Inference (Extended Abstract)
• Session types revisited
• scientific article; zbMATH DE number 7559288 (Why is no real title available?)
• Verifiable abstractions for contract-oriented systems
• On projecting processes into session types
• A Semantics for Propositions as Sessions
• scientific article; zbMATH DE number 7453964 (Why is no real title available?)
• 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
• Session Types with Arithmetic Refinements
• Towards races in linear logic
• Fair subtyping for multi-party session types
• Multiparty session types as coherence proofs
• A core model for choreographic programming
• A subexponential view of domains in session types
• Non-linearity as the metric completion of linearity
• A universal session type for untyped asynchronous communication
• 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
• Non-blocking concurrent imperative programming with session types
• Resource sharing via capability-based multiparty session types
• Session Types with Gradual Typing
• The true concurrency of differential interaction nets

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)