In this blog post, Frank S. de Boer and I write about the proof system that I first introduced in my PhD thesis.

M / 000

In this blog post, Frank S. de Boer and I write about the proof system that I first introduced in my PhD thesis. We introduce the proof system, show a number of examples, argue why it exceeds all current proof systems in capability, and discuss issues in separation logic such as referential transparency, univalence, well-foundedness and finiteness.

(Part of a series: next blog post is about relative completeness of this system.)

dr. heap A sound and complete proof system for separation logic (part 1) – dr. heap A novel proof system for separation logic is explained.

First published on LinkedIn. The blog post is A sound and complete proof system for separation logic (part 1); the day this was posted is not recorded, so the date above is the day that article was published.