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 logicIProp, the standard model of Iris- A selection of the Iris resources, including invariants, later credits, and many more.
MoSeL (in contrast to the older IPM) supports different separation logics as well. For more details on the proofmode, see proofmode.md.
More details about the status of our port can be found on our tracking site.
- 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.url = "https://github.com/leanprover-community/iris-lean.git"
git.subDir = "Iris"
rev = "master"
- To use Iris constructions based on mathlib, you can also import the math library
[[require]]
name = "iris"
git.url = "https://github.com/leanprover-community/iris-lean.git"
git.subDir = "IrisMath"
rev = "master"
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 a team of developers, coordinating on the iris-lean channel on the Lean Zulip.
We always welcome new contributors! For questions, contribution guidance, and development information, feel free to introduce yourself on the Zulip.
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.