diff --git a/CHANGELOG.md b/CHANGELOG.md
index 390d35d6116b1f678ce12913486e8d3d465d525d..a12ad3ffaa078d305db920313fa9960cbf4e951c 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.