## 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