Commit c2247c3a authored by Lennard Gäher's avatar Lennard Gäher
Browse files


parent 4d112423
Pipeline #38800 passed with stage
in 13 minutes and 7 seconds
......@@ -5,8 +5,6 @@ It is based on the Coq development of the [Iris Project](
which includes [MoSeL](, a general proof mode
for carrying out separation logic proofs in Coq.
For understanding the theory of Transfinite Iris, a supplementary appendix PDF has been submitted alongside this artifact.
For using Transfinite Iris and inspecting the development interactively, it needs to be compiled.
## Building Transfinite Iris
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment