considered behavioral types a la SLMC?

kaist-plrg / jiset

JISET: JavaScript IR-based Semantics Extraction Toolchain

38 stars 8 forks source link

considered behavioral types a la SLMC? #201

Open dckc opened 2 years ago

dckc commented 2 years ago

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

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

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

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:

temporal / modal reasoning: eventually / always as in TLA+
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