Is there a concurrent separation logic in Isabelle for imperative language? I found A Separation Logic Framework for Imperative HOL but that's not designed for concurrent imperative language like C and I wonder if there is a such framework as Iris in Coq? Maybe the framework developed by Viktor Vafeiadis is the most relevant one. But I wonder if there is a more well-developed framework that supports better syntax and detailed features. Further, Is there an implementation of RGSep or local rely guarantee in Isabelle?
The closest to Iris in Isabelle is the experimental isariris
Thanks a lot! How about the RGSep or LRG? Are there some implementations in Isabelle?
I don't know about that.
That's ok, you have helped me a lot!
Last updated: Dec 07 2023 at 16:21 UTC