Linear Logic as CSP

摘要

The cut elimination/normalization process in a logical calculus may simulate computations. This amounts to designing a programming language on alogicalcalculus. Typedλ-calculus is a familiar example. Linear logic has been used for simulating both a‘resource sensitive’computation and parallel computations. We investigate how to let linear logic simulate parallel computations. The focus is on the multiplicative fragment in the proof net formalization of linear logic. A translation from such proofs into a corresponding CSP process is offered. It is shown that the translation yields a step-by-step correspondence between the cut elimination process and the CSP execution. Generalizations and related work are discussed. We are concerned with the handling of the failure of the Church–Rosser property. We point out the two possible strategies to adopt: either restrict attention to the cases where the property does hold, or try to give an interpretation where the ordering m