Parallel Tensor

(* protocol *)

sortdef protocol = type

(* binary role *)

sortdef role = {n:int|n==0||n==1}

(* atomics *)

stacst msg: (int, vt@ype) -> protocol

stacst nil: int -> protocol

stacst seq: (protocol, protocol) -> protocol

#define :: seq

(* connectives *)

stacst addi: (int, protocol, protocol) -> protocol // additives: oplus, amp

stacst mult: (int, protocol, protocol) -> protocol // multiplicatives: tensor, parr

(* type constructor *)

absvtype chan (int, protocol)

(* axiom *)

fun create {r:role} {p:protocol} (chan(1-r,p) -<lincloptr1> void): chan(r,p)

(* atomics *)

fun send {r:role} {p:protocol} {v:vt@ype} (!chan(r,msg(r,v)::p) >> chan(r,p), v): void

fun recv {r:role} {p:protocol} {v:vt@ype} (!chan(r,msg(1-r,v)::p) >> chan(r,p)): v

fun wait {r:role} (chan(r,nil(1-r))): void

fun close {r:role} (chan(r,nil r)): void

(* additive connectives *)

datavtype choice (protocol, p:protocol, q:protocol) =

| Left (p,p,q)

| Right (q,p,q)

fun amp {r:role} {p,q:protocol} (!chan(r,addi(1-r,p,q)) >> chan(r,s)): #[s:protocol] choice (s,p,q)

fun oplus {r:role} {p,q,s:protocol} (!chan(r,addi(r,p,q)) >> chan(r,s), choice (s,p,q)): void

(* multiplicative connectives *)

fun tensor {r:role} {p,q:protocol} (chan(r,mult(r,p,q)), chan(r,p) -<lincloptr1> void, chan(r,q) -<lincloptr1> void): void

fun parr {r:role} {p,q:protocol} (chan(r,mult(1-r,p,q))): @(chan(r,p), chan(r,q))

(* cut *)

fun cut {r:role} {p:protocol} (chan(r,p), chan(1-r,p)): void