diff --git a/docs/algebra.tex b/docs/algebra.tex
index 7d18bfab11fffa712c8a9f00cba93acc84b6bd08..1263d0fa75dd1c86525b025480ea3d934f575030 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -2,7 +2,9 @@
\subsection{COFE}
+The model of Iris lives in the category of \emph{Complete Ordered Families of Equivalences} (COFEs).
This definition varies slightly from the original one in~\cite{catlogic}.
+
\begin{defn}[Chain]
Given some set $\cofe$ and an indexed family $({\nequiv{n}} \subseteq \cofe \times \cofe)_{n \in \mathbb{N}}$ of equivalence relations, a \emph{chain} is a function $c : \mathbb{N} \to \cofe$ such that $\All n, m. n \leq m \Ra c (m) \nequiv{n} c (n)$.
\end{defn}
diff --git a/docs/bib.bib b/docs/bib.bib
index 03e1cd6a463713c43f545a2bf59154bfbf181cf3..0f1f4c62da8fb58b872c70967fe708be3c17f4b7 100644
--- a/docs/bib.bib
+++ b/docs/bib.bib
@@ -3577,3 +3577,118 @@ year = {2013}
note = {Available at \url{http://users-cs.au.dk/birke/modures/tutorial/categorical-logic-tutorial-notes.pdf}}
}
+@article{dodds:higher-order-sync,
+ author = {Mike Dodds and
+ Suresh Jagannathan and
+ Matthew J. Parkinson and
+ Kasper Svendsen and
+ Lars Birkedal},
+ title = {Verifying Custom Synchronization Constructs Using Higher-Order Separation
+ Logic},
+ journal = {{ACM} Trans. Program. Lang. Syst.},
+ volume = {38},
+ number = {2},
+ pages = {4},
+ year = {2016},
+ url = {http://doi.acm.org/10.1145/2818638},
+ doi = {10.1145/2818638},
+ timestamp = {Fri, 29 Jan 2016 12:43:32 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/toplas/DoddsJPSB16},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@inproceedings{iris,
+ author = {Ralf Jung and
+ David Swasey and
+ Filip Sieczkowski and
+ Kasper Svendsen and
+ Aaron Turon and
+ Lars Birkedal and
+ Derek Dreyer},
+ title = {Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent
+ Reasoning},
+ booktitle = {POPL},
+ pages = {637--650},
+ year = {2015},
+}
+
+@phdthesis{krebbers:phd,
+ author = {Robbert Krebbers},
+ title = "{The C standard formalized in Coq}",
+ year = {2015},
+ school = {Radboud University},
+}
+
+@inproceedings{garillot:gonthier:mahboubi:rideau:09,
+ author = {Fran{\c{c}}ois Garillot and
+ Georges Gonthier and
+ Assia Mahboubi and
+ Laurence Rideau},
+ title = "{Packaging Mathematical Structures}",
+ booktitle = {TPHOLs},
+ pages = {327--342},
+ series = {LNCS},
+ volume = {5674},
+ year = {2009},
+}
+
+@article{spitters:weegen:11,
+ author = {Bas Spitters and Eelis van der Weegen},
+ title = "{Type classes for mathematics in type theory}",
+ journal = {MSCS},
+ volume = {21},
+ number = {4},
+ pages = {795--825},
+ year = {2011},
+}
+
+@article{sozeau:09,
+ author = {Matthieu Sozeau},
+ title = "{A New Look at Generalized Rewriting in Type Theory}",
+ journal = {Journal of Formalized Reasoning},
+ volume = {2},
+ number = {1},
+ pages = {41--62},
+ year = {2009},
+}
+
+@InProceedings{malecha:esop2016,
+ author = {Gregory Malecha and Jesper Bengtson},
+ title = {Easy and efficient automation through reflective tactics},
+ booktitle = {ESOP},
+ year = 2016,
+}
+
+@inproceedings{gps,
+ author = {Aaron Turon and
+ Viktor Vafeiadis and
+ Derek Dreyer},
+ title = {{GPS:} navigating weak memory with ghosts, protocols, and separation},
+ booktitle = {Proceedings of the 2014 {ACM} International Conference on Object Oriented
+ Programming Systems Languages {\&} Applications, {OOPSLA} 2014,
+ part of {SPLASH} 2014, Portland, OR, USA, October 20-24, 2014},
+ pages = {691--707},
+ year = {2014},
+ url = {http://doi.acm.org/10.1145/2660193.2660243},
+ doi = {10.1145/2660193.2660243},
+ timestamp = {Thu, 16 Oct 2014 09:16:18 +0200},
+ biburl = {http://dblp.uni-trier.de/rec/bib/conf/oopsla/TuronVD14},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@article{birkedal:metric-space,
+ author = {Lars Birkedal and
+ Kristian St{\o}vring and
+ Jacob Thamsborg},
+ title = {The category-theoretic solution of recursive metric-space equations},
+ journal = {Theor. Comput. Sci.},
+ volume = {411},
+ number = {47},
+ pages = {4102--4122},
+ year = {2010},
+ url = {http://dx.doi.org/10.1016/j.tcs.2010.07.010},
+ doi = {10.1016/j.tcs.2010.07.010},
+ timestamp = {Tue, 07 Dec 2010 16:23:22 +0100},
+ biburl = {http://dblp.uni-trier.de/rec/bib/journals/tcs/BirkedalST10},
+ bibsource = {dblp computer science bibliography, http://dblp.org}
+}
diff --git a/docs/iris.sty b/docs/iris.sty
index 8b0cb49dbdba6af5a63e593ca2d115031bb8dacf..f86e50a3b152932500c37086278a622a94731d36 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -36,7 +36,7 @@
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
-\newcommand{\spac}{\;} % a space
+\newcommand{\spac}{\,} % a space
\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
@@ -292,6 +292,7 @@
%% Some commonly used identifiers
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
+\newcommand{\persistent}[1]{\textlog{persistent}(#1)}
\newcommand{\physatomic}[1]{\textlog{atomic}($#1$)}
\newcommand{\infinite}{\textlog{infinite}}
@@ -362,7 +363,7 @@
\tikzstyle{sts_arrows} = [arrows={->[scale=1.5]},every node/.style={font=\sffamily\small}]
%% Stored Propositions
-\newcommand{\mapstoprop}{\mathrel{\mapstochar\Ra}}
+\newcommand{\mapstoprop}{\mathrel{\kern-0.5ex\tikz[baseline=(m)]{\node at (0,0) (m){}; \draw[line cap=round] (0,0.16) -- (0,-0.004);}\kern-1.5ex\Ra}}
\endinput
diff --git a/docs/model.tex b/docs/model.tex
index ea2a89bdc89af2ed6f544bbb4c4a4a10d29c5add..1fdab67f8741caab6cb330a72bd9aa607d3c0b63 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -60,7 +60,7 @@ Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}(-)$.
Now we can write down the recursive domain equation:
\[ \iPreProp \cong \UPred(\textdom{ResF}(\iPreProp)) \]
-$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89}.
+$\iPreProp$ is a COFE, which exists by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}.
We do not need to consider how the object is constructed.
We only need the isomorphism, given by
\begin{align*}