considered behavioral types a la SLMC?

[dckc]

Have you considered behavioral types a la SLMC?

• Luís Caires, Behavioral and Spatial Observations in a Logic for the Pi-Calculus, FoSSaCS 2004, ETAPS 2004, Barcelona, 2004.

I have done a little work toward porting it to scala: https://github.com/rchain-community/behavr

Would you please help me find your current code for type analysis?

I hope you don't mind my use of your issues list for half-baked ideas...

[jhnaldo]

Hi, @dckc. Thanks for the good suggestion related to the behavioral types. Unfortunately, I'm not familiar with this concept. If you give us more information we can discuss it deeper. For the type analysis, we have another repository: https://github.com/kaist-plrg/jstar. We recommend you look around this repo.

[dckc]

http://ctp.di.fct.unl.pt/SLMC/ has papers, code, examples, and such. Most everything I know about it came from there, so I can't think of a way to give you more information, unless perhaps our groups meet again soonish and we can discuss it.

I will definitely check out JSTAR... ooh! refinement types! excellent...

[dckc]

JSTAR is even more fantastic on close examination... refinement types and abstract interpretation. wonderful!

The two features of SLMC that I don't see are:

1. temporal / modal reasoning: eventually / always as in TLA+
2. the new construct, i.e. freshness, composed with the parallel operator in pi-calculus, which allows reasoning such as:

defprop everybody_knows(secret) = everywhere(@secret);

defprop everybody_gets_to_know = 
    hidden secret.eventually everybody_knows(secret);

-- http://ctp.di.fct.unl.pt/SLMC/examples/gossip.html , http://ctp.di.fct.unl.pt/SLMC/examples/gossip_info.html