Conversation

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?

researchgate.net

(PDF) Proof Tactics for Assertions in Separation Logic

PDF | This paper presents tactics for reasoning about the assertions of separation logic. We formalise our proof methods in Isabelle/HOL based on... | Find, read and cite all the research you need on...

Brendan Zabarauskas

@brendanzab

Replying to

@kamatsu8

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?

12:22 AM · Sep 29, 2021Twitter Web App

Replying to

Nope, having never used Lean 4 nor read PLFCC

Liam O'Connor

@kamatsu8

Sep 29, 2021

I know, surprising, considering my research was, for years, all about certified compilers

Show replies