From 9bd742a22847f623c82b22b8dc7366ae4ea72fcc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Aug 2019 20:01:41 +0200
Subject: [PATCH] add links
---
CHANGELOG.md | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 390d35d61..a12ad3ffa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -15,7 +15,12 @@ Chajed. Thanks a lot to everyone involved!
The highlight of this release is the completely re-engineered interactive proof
mode. Not only did many tactics become more powerful; the entire proof mode can
now be used not just for Iris but also for other separation logics satisfying
-the proof mode interface.
+the proof mode interface (e.g., [Iron] and [GPFSL]). Also see the
+[accompanying paper][MoSeL].
+
+[Iron]: https://iris-project.org/iron/
+[GPFSL]: https://gitlab.mpi-sws.org/iris/gpfsl/
+[MoSeL]: https://iris-project.org/mosel/
Beyond that, the Iris program logic gained the ability to reason about
potentially stuck programs, and a significantly strengthened adequacy theorem
@@ -92,8 +97,7 @@ Changes in heap_lang:
Changes in Coq:
-* An all-new generalized proof mode that abstracts away from Iris! See
- <http://iris-project.org/mosel/> for the corresponding paper. Major new
+* An all-new generalized proof mode that abstracts away from Iris! Major new
features:
- The proof mode can now be used with logics derived from Iris (like iGPS),
with non-step-indexed logics and even with non-affine (i.e., linear) logics.
--
GitLab