An exact correspondence between a typed pi-calculus and polarised proof-nets

DOI10.1016/j.tcs.2010.01.028zbMath1203.68114OpenAlexW2085264580MaRDI QIDQ974114

Olivier Laurent, Kohei Honda

Publication date: 27 May 2010

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2010.01.028

zbMATH Keywords

typesdeterminismembeddinglogicslinear logicinteractionconcurrencypolaritypi-calculusnon-determinismproofsprocessesproof-nets

Mathematics Subject Classification ID

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

Related Items (9)

Non-linearity as the Metric Completion of Linearity ⋮ Conflation Confers Concurrency ⋮ The true concurrency of differential interaction nets ⋮ Jump from parallel to sequential proofs: exponentials ⋮ Unnamed Item ⋮ A Truly Concurrent Game Model of the Asynchronous $$\pi $$-Calculus ⋮ Typed event structures and the linear \(\pi \)-calculus ⋮ Linear logic propositions as session types ⋮ Interpreting a finitary pi-calculus in differential interaction nets

Cites Work

• Linear logic
• Strong normalisation in the \(\pi\)-calculus
• Computational interpretations of linear logic
• Differential interaction nets
• A calculus of mobile processes. II
• An equivalence between lambda- terms
• Proofs as processes
• On the \(\pi\)-calculus and linear logic
• On reduction-based process semantics
• Polarized proof-nets and \(\lambda \mu\)-calculus
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• The name discipline of uniform receptiveness
• Syntax vs. semantics: A polarized approach
• Locus Solum: From the rules of logic to the logic of rules
• Bigraphs and transitions
• Process Algebra
• Functions as processes
• πI: A symmetric calculus based on internal mobility
• Computer Science Logic
• Behavioral equivalence in the polymorphic pi-calculus
• CONCUR 2005 – Concurrency Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An exact correspondence between a typed pi-calculus and polarised proof-nets