[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