Concurrent Processes as Wireless Proof Nets
Source: University of Paris 13
The authors present a proofs-as-programs correspondence between linear logic and process calculi that permits non-deterministic behaviors. Processes are translated into wireless proof nets, i.e. proof nets of multiplicative linear logic without cut wires. Typing a term using them consists in typing some of its possible determinisations in standard sequent calculus. Generalized cut-elimination steps in wireless proof nets are shown to correspond to executions that avoid deadlocks. Proof nets were introduced with linear logic as its natural proof syntax, and the graphical formulation of cut elimination in them emphasizes the fact that linear logic is logic of interaction.