Stream: Is there code for X?

Topic: concurrent separation logic

view this post on Zulip HuanSun (Nov 25 2022 at 12:28):

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?

view this post on Zulip Fabian Huch (Nov 25 2022 at 12:36):

The closest to Iris in Isabelle is the experimental isariris

view this post on Zulip HuanSun (Nov 25 2022 at 13:21):

Thanks a lot! How about the RGSep or LRG? Are there some implementations in Isabelle?

view this post on Zulip Fabian Huch (Nov 25 2022 at 13:44):

I don't know about that.

view this post on Zulip HuanSun (Nov 25 2022 at 13:47):

That's ok, you have helped me a lot!

Last updated: Dec 21 2024 at 16:20 UTC