
The multiplicative fragment of linear logic is studied with the aim to simulate parallel computations. A translation is defined which transforms proofs of this formalism into communicating sequential processes (CSP). This translation is determined by a step-by-step correspondence between the cut-elimination process and the CSP execution. In section 3 a detailed description of this correspondence is given based on two maps \(t(-)\) and \(e(-)\). \(t\) maps proof nets into CSP processes, and \(e(-)\) executes the process \(t(P)\) one step according to the rules of CSP. The proof of correctness of this correspondence, presented in section 4, makes use of an inverse map \(i(-)\), which takes as arguments the result after execution of the process \(t(P)\) one step, and produces a proof net \(P'\) such that \(i(e(t(P)))= P'\) and \(r(P)= P'\), where \(r(-)\) is the reduction step determined by the elimination process associated with the fragment under consideration. The correctness theorem states that \(r(P)= i(e(t(P)))\). The paper presents a valuable interpretation of normalizations of proof nets as parallel computations in CSP.
multiplicative fragment of linear logic, correctness, normalization of proof nets, simulation of parallel computation, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), communicating sequential processes, cut-elimination, Cut-elimination and normal-form theorems, Models of computation (Turing machines, etc.), Subsystems of classical logic (including intuitionistic logic)
multiplicative fragment of linear logic, correctness, normalization of proof nets, simulation of parallel computation, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), communicating sequential processes, cut-elimination, Cut-elimination and normal-form theorems, Models of computation (Turing machines, etc.), Subsystems of classical logic (including intuitionistic logic)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
