use cases: confinement, liveness from Namespaces, LADL

[dckc]

We also exhibit nontrivial formulae encoding confinement and liveness properties for a reflective
higher-order variant of the π-calculus.
-- LADL

[dckc]

found the liveness formula:

µX.recv(⊤, x → X) | ⊤

in rholang, recv(n, x -> P) is for(x <- n) { P }

So... inferring implicit quotation of ⊤ when used in a name context, this is something like...

µX.for(x <- @True) { X } | True

but I'm not sure what to do with µ.

[dckc]

firewall / confinement:

µX.recv(“φ”, x → (X ∨ 0) | ¬recv(“¬φ”, ⊤)) | ¬recv(“¬φ”, ⊤)

type Firewall(phi) = mu X. for(x <- phi) { X or Zero  | Not(for(_ <- @Not(phi)) { True }) }
   | Not(for(_ <- @Not(phi) ) { True })