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
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.
2
There's a bunch of separation logic stuff an it's a bit bewildering tbh