Linear logic propositions as session types

DOI10.1017/S0960129514000218zbMath1361.68162OpenAlexW2025260761MaRDI QIDQ5741566

Bernardo Toninho, Luís Caires, Frank Pfenning

Publication date: 28 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129514000218

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) 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 (30)

On concurrent behaviors and focusing in linear logic ⋮ Mixed Sessions ⋮ Multiparty session types, beyond duality ⋮ A practical type theory for symmetric monoidal categories ⋮ Comparing type systems for deadlock freedom ⋮ Unnamed Item ⋮ Event structure semantics for multiparty sessions ⋮ Session-based concurrency in Maude: executable semantics and type checking ⋮ Extracting total Amb programs from proofs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Linearity, Control Effects, and Behavioral Types ⋮ Unnamed Item ⋮ Nested session types ⋮ Fundamentals of session types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A message-passing interpretation of adjoint logic ⋮ Mixed sessions ⋮ Session-typed concurrent contracts ⋮ Session Types with Arithmetic Refinements ⋮ Probabilistic Analysis of Binary Sessions ⋮ Hybrid linear logic, revisited ⋮ Constructing weak simulations from linear implications for processes with private names ⋮ Processes against tests: on defining contextual equivalences ⋮ Polymorphic lambda calculus with context-free session types ⋮ A focused linear logical framework and its application to metatheory of object logics

Cites Work

• Linear logic
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Computational interpretations of linear logic
• An exact correspondence between a typed pi-calculus and polarised proof-nets
• Linearity and bisimulation
• On the expressiveness of internal mobility in name-passing calculi
• On the \(\pi\)-calculus and linear logic
• A linear logical framework
• Subtyping for session types in the pi calculus
• Session Types as Intuitionistic Linear Propositions
• A Linear Account of Session Types in the Pi Calculus
• Logical Semantics of Types for Concurrency
• Functions as processes
• On asynchrony in name-passing calculi
• Correspondence assertions for process synchronization in concurrent communications

This page was built for publication: Linear logic propositions as session types