Cut reduction in linear logic as asynchronous session-typed communication

DOI10.4230/LIPICS.CSL.2012.228MaRDI QIDQ4649549zbMATH OpenFDO

Authors Henry DeYoung, Luís Caires, Bernardo Toninho, Frank Pfenning

Publication date 22 November 2012

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2012.228

zbMATH Keywords

asynchronous pi-calculuscut reductionlinear logicsession types

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
• Session types as intuitionistic linear propositions
• Linear type theory for asynchronous session types
• A new linear logic for deadlock-free session-typed processes
• Linear logical relations for session-based concurrency

Cited in

(14)

• A message-passing interpretation of adjoint logic
• Mechanizing focused linear logic in Coq
• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Substructural proofs as automata
• Rast: a language for resource-aware session types
• Circular proofs as session-typed processes: a local validity condition
• Domain-aware session types
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Comparing session type systems derived from linear logic
• Deadlock freedom for asynchronous and cyclic process networks
• A subexponential view of domains in session types
• Rast: resource-aware session types with arithmetic refinements (system description)
• A gentle overview of asynchronous session-based concurrency: deadlock freedom by typing
• Object-level reasoning with logics encoded in HOL Light

This page was built for publication: Cut reduction in linear logic as asynchronous session-typed communication

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