Lean 4 port of Iris, a higher-order concurrent separation logic framework.
"Iris is a framework that can be used for reasoning about safety of concurrent programs, as the logic in logical relations, to reason about type-systems, data-abstraction etc."
– https://iris-project.org/
Rocq formalization of Iris: https://gitlab.mpi-sws.org/iris/iris/
Currently, Iris-Lean has support for
- MoSeL, the proof interface of Iris
UPred, the Iris base logic- A selection of the Iris resources
MoSeL (in contrast to the older IPM) supports different separation logics as well. For more details on the proofmode, see proofmode.md.
- Iris-Lean is updated in sync with Lean. The releases page includes tags for recent versions.
- The
masterbranch may contain features added since the last release:
[[require]]
name = "iris"
git = "https://github.com/leanprover-community/iris-lean.git"
rev = "master"
- The
unstabletag will be periodically updated with features that are still in development:
[[require]]
name = "iris"
git = "https://github.com/leanprover-community/iris-lean.git"
rev = "unstable"
This project started as part of Lars König's master's thesis at Karlsruhe Institute of Technology (KIT). It is currently being maintained by Mario Carneiro and Markus de Medeiros.
For questions, contribution guidance, and development information, see the iris-lean channel on the Lean Zulip. We always welcome new contributors, and would be happy to help you find something to work on!
Most of the unicode characters used in Iris can be written with the Lean extension replacement, e.g. \ast will automatically be replaced with ∗. To add additional replacements, edit the Lean extension setting lean4.input.customTranslations. Suggested additional replacements are listed below.
"sep": "∗",
"wand": "-∗",
"pure": "⌜⌝",
"bientails": "⊣⊢"- koenig22, Master Thesis, An Improved Interface for Interactive Proofs in Separation Logic, 2022-10, Lars König, KIT.