On the pi-Calculus and Linear Logic

G Bellin and P J Scott

Abstract: We detail Abramsky's ``proofs-as-processes'' paradigm for interpreting classical linear logic (CLL) into a ``synchronous'' version of the pi-calculus recently proposed by Milner. The translation is given at the abstract level of proof structures. We give a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. We also give Soundness and completeness results for the process-calculus translations of various fragments of CLL. The paper also gives a self-contained introduction to some of the deeper proof-theory of CLL, and its process interpretation.

LFCS report ECS-LFCS-92-232

A revised version will appear in Theoretical Computer Science (1994), Proceedings Mathematical Foundations of Programming Semantics 8 (MFPS 8).

Previous | Index | Next