Separation Logic

Stream: lean4

[Sebastian Ullrich]

I think this deserves a separate topic: @Lars König has just defended his master thesis, in which he ported (a big chunk of) the separation logic interface of the Coq library Iris to Lean 4, including some surface & internal improvements (see ch. 5 for a comparison) https://pp.ipd.kit.edu/uploads/publikationen/koenig22masterarbeit.pdf image.png

[Lars König]

Thank you @Sebastian Ullrich :) The code is now available at iris-lean for everyone interested. The readme file describes how one can use the proof interface to perform proofs in a custom separation logic. It also explains some concepts and the structure of the project. There are examples for classical separation logic in src/Iris/Instances/Classical and the proof from the image above can be found in src/Iris/Examples/Proofs.lean.