Introduction

Par is affectionatelly named after the most bemusing connective of linear logic: ⅋, pronounced “par”. That’s because Par is based directly on (classical) linear logic, as an experiment to see where this paradigm can take us.

Jean-Yves Girard — the author of linear logic, and System F, among other things — wrote on the page 3 of his first paper on linear logic:

The new connectives of linear logic have obvious meanings in terms of parallel computation, especially the multiplicatives.

This was in 1987. In hindsight, it wasn’t that obvious. What’s obvious is that it is there — the parallel computation, that is. What isn’t obvious at all is how to turn it into a practical programming language.

TODO