[Iris-Club] Technical Documentation available

Ralf Jung jung at mpi-sws.org
Thu Mar 17 17:10:51 CET 2016


Hi all,

The Iris git repository at <https://gitlab.mpi-sws.org/FP/iris-coq/> now
contains an up-to-date LaTeX version of the logic. The document at
`docs/iris.tex` defines the algebraic structures Iris relies on, the
core proof rules, their model, and some derived forms.
This is a "mathematical" presentation, so some things are set up
slightly differently than in Coq. However, I only made changes that are
"obviously" isomorphic to the Coq definitions.

If you find any issues, feel free to report them here on the list or in
our issue tracker: <https://gitlab.mpi-sws.org/FP/iris-coq/issues>.

Kind regards,
Ralf




More information about the Iris-Club mailing list