Cut reduction in linear logic as asynchronous session-typed communication

DOI10.4230/LIPICS.CSL.2012.228zbMATH Open1252.03141MaRDI QIDQ4649549FDOQ4649549

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

Publication date: 22 November 2012

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

zbMATH Keywords

linear logicsession typesasynchronous pi-calculuscut reduction

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 (11)

• Session typing and asynchronous subtyping for the higher-order \(\pi\)-calculus
• Title not available (Why is that?)
• Substructural proofs as automata
• A message-passing interpretation of adjoint logic
• Circular proofs as session-typed processes: a local validity condition
• Title not available (Why is that?)
• Mechanizing focused linear logic in Coq
• Asynchronous session-based concurrency: deadlock-freedom in cyclic process networks
• Deadlock freedom for asynchronous and cyclic process networks
• Comparing session type systems derived from linear logic
• A subexponential view of domains in session types

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)