I really want *someone else* to implement this in Lean so I can go back to the original reason I took this venture into separation logic (my 6502 verification framework)
Any volunteers?
Conversation
This would be neat! I've been wanting to play around with separation logic in Lean. I was thinking of trying to port some of the stuff in “Program Logics for Certified Compilers” at some stage to Lean 4… do you know how this stuff compares?
1
Nope, having never used Lean 4 nor read PLFCC
1
I know, surprising, considering my research was, for years, all about certified compilers
1
Replying to
Haha, no worries! Like, just curious if there was something special you were wanting in separation logic that is mentioned in this paper in particular.
There's a bunch of separation logic stuff an it's a bit bewildering tbh
Replying to
I have it on good authority that this stuff is the state of the art in proof calculi for SL, and (as the paper suggests) it certainly improves on the Isabelle infrastructure my old group produced. And the tactics are for BI-assertions, which is what I want, not SL triples.
1