use cases: confinement, liveness from Namespaces, LADL

rchain-community / behavr

Toward Behavioral Type checking for Rholang

Apache License 2.0

6 stars 1 forks source link

Open dckc opened 5 years ago

dckc commented 5 years ago

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

dckc commented 5 years ago

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 commented 5 years ago

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 })