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.
A revised version will appear in Theoretical Computer Science (1994), Proceedings Mathematical Foundations of Programming Semantics 8 (MFPS 8).
Previous | Index | Next