Correspondence of Par and linear logic

[faiface]

Since it was requested, I'm sketching here the correspondence between Par and linear logic. I will refine it over time.

Par is primarily based on a little process language called CP from Phil Wadler's paper "Propositions as Sessions".

The correspondence with linear logic is best shown via typing. While Par is dynamically typed, a type system lives in its spirit because every operation actually corresponds to a proof-line in linear logic's sequent calculus. All programs that will be typeable in the future can be given types now and type-checked on paper without any changes to the language.

There are two syntactic modes in Par: processes and expressions.

Processes are typeable by usual sequents (like |- A, B, C), with all propositions having an equal position, none distinguished. Processes don't have any special result type, they just end after handling all of their variables.

Expressions are typeable by sequents with a distinguished result proposition, such as |- A | B, C, D, here A being the result type. I separate the distinguished variable by a pipe.

Let's adopt this ASCII terminology for linear logic:

• ** is "times"/"tensor"
• || is "par"
• + is "plus"
• & is "with"
• 1, F, T, 0 are units of **, ||, &, + respectively
• ~ is linear negation

Let's only consider a subset of Par's syntax:

• Expressions of the form
  • <name>
  • chan <name> { <process> }
• Commands of the form:
  • <name>! - Closing a channel
  • <name>? - Waiting for the other side to close a channel
  • <name>(<expression>) - Sending a value
  • <name>[<name>] - Receiving a value
  • <name>.left / <name>.right - Sending a signal
  • <name> { left => { <process> } right => { <process> } } - Receiving a signal
  • <name> { } - Blocking forever on no signal possible (means unreachable point)

The typing sequents then have this form:

• Expression typing sequent: <expression> |- <result type> | <name> : <type>, ...
• Process typing sequent: <process> |- <name> : <type>, ...

The <name> : <type> judgements are the context of free variables at that point.

G, and H will be contexts (sequences of variables judgments), P, Q will denote processes, E will be an expression, A, B will be types, and x, y will be variables. The typing rules then look like this:

---------------
x |- A | x : ~A


           P |- G, x : A
------------------------
chan x { P } |- A | G


-----------
x! |- x : 1


   P |- G
----------------
x? P |- G, x : F


E |- A | G   P |- H, x : B
--------------------------
x(E) P |- G, H, x : A ** B


     P |- G, y : A, x : B
-------------------------
x[y] P |- G, x : A || B


       P |- G, x : A
------------------------
x.left P |- G, x : A + B


        P |- G, x : B
------------------------
x.right P |- G, x : A + B


     P |- G, x : A             Q |- G, x : B     
-------------------------------------------------
x { left => { P } right => { Q }} |- G, x : A & B


-----------------
x { } |- G, x : T

Hopefully I didn't make a mistake. I can possibly also attach a PDF with the rules, if this is too unreadable.

All other constructs (such as expression syntax) in Par are made from these basic operations, so their typing should follow from their translation to these basic rules.

[4ad]

Wonderful, thanks!