© 1994 by Oxford University Press
Original Articles |
Linear Logic as CSP
Department of Informatics, University of Trondheim 7055 Dragvoll, Norway E-mail: EricMonteiro{at}ifi.unit.no
The cut elimination/ normalization process in a logical calculus may simulate computations. This amounts to designing a programming language on a logical calculus. 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 ChurchRosser 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 matters.
Keywords: Simulating computations in logic,; linear logic,; cut elimination in proof nets,; parallel processing.; ChurchRosser property.