Linear logic is a hot research topic in the theoretical foundations of programming language. This paper presents some interesting results and methodological insights about several fragments of multiplicative linear logic within a natural deduction framework. In functional programming, the Curry-Howard isomorphism relates natural deduction intuitionistic proofs and their normalizations to programs and their execution. In logic programming, it allows the presentation of some relevant results, such as permutability and uniform proofs.

The authors propose new natural deductive systems of linear logic for various forms of the par connective. This connective has not seemed amenable to natural deduction, because it has appeared to be impossible to formulate adequate introduction and elimination rules for par in single conclusion systems. Starting from a simple implicative fragment, and adding more connectives step by step, the authors show that there can be natural deduction systems that cope with par.

The authors of this concise paper state the purpose and results of their work clearly. The methodology will be encouraging to researchers in this area.