ON THE PI-CALCULUS AND LINEAR LOGIC

We detail Abramsky's ''proofs-as-processes'' paradigm for interpreting classical linear logic (CLL) (Girard, 1987) into a ''synchronous'' ve rsion of the pi-calculus recently proposed by Milner (1992, 1993). The translation is given at the abstract level of proof structures. We gi ve a detailed treatment of information flow in proof-nets and show how to mirror various evaluation strategies for proof normalization. We a lso give soundness and completeness results for the process-calculus t ranslations of various fragments of CLL. The paper also gives a self-c ontained introduction to some of the deeper proof-theory of CLL, and i ts process interpretation.