diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index 54e771682676a8329793da45ea1ce9d8e308c206..4141e9e45fc2a8599ee3ee08259b6c208c313674 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -107,8 +107,6 @@ Inductive expr :=
   | InjL (e : expr)
   | InjR (e : expr)
   | Case (e0 : expr) (e1 : expr) (e2 : expr)
-  (* Concurrency *)
-  | Fork (e : expr)
   (* Heap *)
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Free (e : expr)
@@ -117,6 +115,8 @@ Inductive expr :=
   | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
   | Xchg (e0 : expr) (e1 : expr) (* exchange *)
   | FAA (e1 : expr) (e2 : expr) (* Fetch-and-add *)
+  (* Concurrency *)
+  | Fork (e : expr)
   (* Prophecy *)
   | NewProph
   | Resolve (e0 : expr) (e1 : expr) (e2 : expr) (* wrapped expr, proph, val *)
@@ -243,7 +243,6 @@ Proof.
      | InjR e, InjR e' => cast_if (decide (e = e'))
      | Case e0 e1 e2, Case e0' e1' e2' =>
         cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
-     | Fork e, Fork e' => cast_if (decide (e = e'))
      | AllocN e1 e2, AllocN e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
      | Free e, Free e' =>
@@ -257,6 +256,7 @@ Proof.
         cast_if_and (decide (e0 = e0')) (decide (e1 = e1'))
      | FAA e1 e2, FAA e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
+     | Fork e, Fork e' => cast_if (decide (e = e'))
      | NewProph, NewProph => left _
      | Resolve e0 e1 e2, Resolve e0' e1' e2' =>
         cast_if_and3 (decide (e0 = e0')) (decide (e1 = e1')) (decide (e2 = e2'))
@@ -410,6 +410,11 @@ Canonical Structure valO := leibnizO val.
 Canonical Structure exprO := leibnizO expr.
 
 (** Evaluation contexts *)
+(** Note that [ResolveLCtx] is not by itself an evaluation context item: we do
+not reduce directly under Resolve's first argument. We only reduce things nested
+further down. Once no nested contexts exist any more, the expression must take
+exactly one more step to a value, and Resolve then (atomically) also uses that
+value for prophecy resolution.  *)
 Inductive ectx_item :=
   | AppLCtx (v2 : val)
   | AppRCtx (e1 : expr)
@@ -498,7 +503,6 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | InjL e => InjL (subst x v e)
   | InjR e => InjR (subst x v e)
   | Case e0 e1 e2 => Case (subst x v e0) (subst x v e1) (subst x v e2)
-  | Fork e => Fork (subst x v e)
   | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
   | Free e => Free (subst x v e)
   | Load e => Load (subst x v e)
@@ -506,6 +510,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst x v e0) (subst x v e1) (subst x v e2)
   | FAA e1 e2 => FAA (subst x v e1) (subst x v e2)
+  | Fork e => Fork (subst x v e)
   | NewProph => NewProph
   | Resolve ex e1 e2 => Resolve (subst x v ex) (subst x v e1) (subst x v e2)
   end.
@@ -661,8 +666,6 @@ Inductive head_step : expr → state → list observation → expr → state →
      head_step (Case (Val $ InjLV v) e1 e2) σ [] (App e1 (Val v)) σ []
   | CaseRS v e1 e2 σ :
      head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
-  | ForkS e σ:
-     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
   | AllocNS n v σ l :
      (0 < n)%Z →
      (∀ i, (0 ≤ i)%Z → (i < n)%Z → σ.(heap) !! (l +ₗ i) = None) →
@@ -707,6 +710,8 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV $ LitInt i1) (state_upd_heap <[l:=Some $ LitV (LitInt (i1 + i2))]>σ)
                []
+  | ForkS e σ:
+     head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
   | NewProphS σ p :
      p ∉ σ.(used_proph_id) →
      head_step NewProph σ
diff --git a/iris_staging/heap_lang/interpreter.v b/iris_staging/heap_lang/interpreter.v
index eca5ef4243fd92c9a968b98b7ee5471bbfac0ecc..322b43439990e8fcabaaae4c42f329c41cdf1fd0 100644
--- a/iris_staging/heap_lang/interpreter.v
+++ b/iris_staging/heap_lang/interpreter.v
@@ -749,15 +749,15 @@ Section interpret_ok.
       (repeat case_match; subst; try errored;
        success;
        eauto using state_wf_upd).
-    - constructor; intros.
-      simpl.
-      apply state_wf_holds; auto.
     - match goal with
       | H: interp_alloc _ _ = (_, _) |- _ => invc H
       end.
       apply state_wf_init_alloc; eauto.
       lia.
     - apply state_wf_same_dom; eauto.
+    - constructor; intros.
+      simpl.
+      apply state_wf_holds; auto.
   Qed.
 
   Local Hint Resolve interpret_wf : core.
@@ -792,13 +792,6 @@ Section interpret_ok.
       lazymatch goal with
       | |- context[Case (Val ?v)] => destruct v; try errored; step_atomic; eauto
       end.
-    - (* Fork *)
-      eapply rtc_once. exists [].
-      lazymatch goal with
-      | |- context[Fork ?e] => eapply (step_atomic _ _ _ _ [e] []); simpl; eauto
-      end.
-      apply head_prim_step; simpl.
-      eauto using head_step.
     - (* AllocN *)
       lazymatch goal with
       | H: interp_alloc _ _ = _ |- _ => invc H
@@ -806,6 +799,13 @@ Section interpret_ok.
       eapply atomic_step. constructor; auto; intros.
       simpl. apply state_wf_holds; eauto.
       simpl; lia.
+    - (* Fork *)
+      eapply rtc_once. exists [].
+      lazymatch goal with
+      | |- context[Fork ?e] => eapply (step_atomic _ _ _ _ [e] []); simpl; eauto
+      end.
+      apply head_prim_step; simpl.
+      eauto using head_step.
   Qed.
 
   (** * Theory for expressions that are stuck after some execution steps. *)
diff --git a/tex/bib.bib b/tex/bib.bib
index a8f88cf36dc4d36cecc3593fcfc196b49c4156af..240bf697b940cdeb9ff95e053445934838b9ac4c 100644
--- a/tex/bib.bib
+++ b/tex/bib.bib
@@ -3849,3 +3849,20 @@ year = {2013}
  volume = {20},
  year = {1955}
 }
+
+@article{iris:prophecy,
+  author    = {Ralf Jung and
+               Rodolphe Lepigre and
+               Gaurav Parthasarathy and
+               Marianna Rapoport and
+               Amin Timany and
+               Derek Dreyer and
+               Bart Jacobs},
+  title     = {The future is ours: prophecy variables in separation logic},
+  journal   = {{PACMPL}},
+  volume    = {4},
+  number    = {{POPL}},
+  doi       = {10.1145/3371113},
+  pages     = {45:1--45:32},
+  year      = {2020}
+}
diff --git a/tex/heaplang.sty b/tex/heaplang.sty
new file mode 100644
index 0000000000000000000000000000000000000000..50e739113bcafef1310c50c62cb40839b2301bdd
--- /dev/null
+++ b/tex/heaplang.sty
@@ -0,0 +1,84 @@
+\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+\ProvidesPackage{heaplang}
+
+\RequirePackage{marvosym}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% CONCRETE LANGUAGE SYNTAX AND SEMANTICS
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\textlang}[1]{\texttt{#1}}
+
+\newcommand{\ProphId}{\textdom{ProphId}}
+
+\newcommand{\langkw}[1]{\textlang{\bfseries #1}}
+\newcommand{\langv}[1]{\ensuremath{\mathit{#1}}} % Yes, this makes language-level variables look like logic-level variables. but we still distinguish locally bound variables from global definitions.
+\newcommand{\lvar}{\langv{\var}}
+\newcommand{\lvarB}{\langv{\varB}}
+\newcommand{\lvarC}{\langv{\varC}}
+\newcommand{\lvarF}{\langv{f}}
+
+\newcommand{\loc}{\ell}
+\newcommand{\prophid}{p}
+
+\newcommand{\stateHeap}{\textproj{heap}}
+\newcommand{\stateProphs}{\textproj{prophs}}
+
+\newcommand\exprForm{{\langkw{e}}}
+\newcommand\valForm{{\langkw{v}}}
+
+\def\Let#1=#2in{\langkw{let} \spac #1 \mathrel{=} #2 \spac \langkw{in} \spac}
+\def\If#1then{\langkw{if} \spac #1 \spac \langkw{then} \spac}
+\def\Else{\spac\langkw{else} \spac}
+\def\Ref(#1){\langkw{ref}(#1)}
+\def\Rec#1(#2)={\langkw{rec}\spac{#1}({#2}) \mathrel{=} }
+\def\RecE#1(#2)={\langkw{rec}_\exprForm\spac{#1}({#2}) \mathrel{=} }
+\def\RecV#1(#2)={\langkw{rec}_\valForm\spac{#1}({#2}) \mathrel{=} }
+\def\Skip{\langkw{skip}}
+\def\Assert{\langkw{assert}}
+\def\Inl{\langkw{inl}}
+\def\Inr{\langkw{inr}}
+\def\Fst{\langkw{fst}}
+\def\Snd{\langkw{snd}}
+\def\True{\langkw{true}}
+\def\False{\langkw{false}}
+\def\NewProph{\langkw{newproph}}
+\def\ResolveWith#1at#2to#3{\langkw{resolve}\spac\langkw{with}\spac#1\spac\langkw{at}\spac#2\spac\langkw{to}\spac#3}
+\def\Resolve#1to#2{\langkw{resolve}\spac#1\spac\langkw{to}\spac#2}
+\def\Match#1with#2=>#3|#4=>#5end{\langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\mid#4\Ra#5\spac\langkw{end}}
+\def\MatchML#1with#2=>#3|#4=>#5end#6{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+    \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+    &#2&\Ra#3\\|&#4&\Ra#5\\%
+    \multicolumn{3}{l}{\langkw{end}#6}%
+  \end{array}}}
+\def\MatchMLL#1with#2=>#3|#4=>#5|#6=>#7end#8{{\arraycolsep=1.4pt\begin{array}[t]{rll}%
+    \multicolumn{3}{l}{\langkw{match}\spac#1\spac\langkw{with}}\\%
+    &#2&\Ra#3\\|&#4&\Ra#5\\|&#6&\Ra#7\\%
+    \multicolumn{3}{l}{\langkw{end}#8}%
+  \end{array}}}
+\def\MatchS#1with#2=>#3end{
+  \langkw{match}\spac#1\spac\langkw{with}\spac#2\Ra#3\spac\langkw{end}}
+
+\newcommand\Alloc{\langkw{Alloc}}
+\newcommand\Free{\langkw{Free}}
+\newcommand\CAS{\langkw{CAS}}
+\newcommand\CmpXchg{\langkw{CmpXchg}}
+\newcommand\Xchg{\langkw{Xchg}}
+\newcommand\FAA{\langkw{FAA}}
+\newcommand\deref{\mathop{!}}
+\let\gets\leftarrow
+
+\newcommand*\Fork[1]{\langkw{fork}\spac\set{#1}}
+
+\newcommand{\fold}{\langkw{fold}\spac}
+\newcommand{\unfold}{\langkw{unfold}\spac}
+
+\newcommand{\HLOp}{\circledcirc}
+\newcommand{\Ptradd}{\mathop{+_{\langkw{L}}}}
+
+\newcommand{\TT}{()}
+\newcommand*\poison{\text{\Biohazard}}
+
+\newcommand\valeq{\cong}
+\newcommand\valne{\ncong}
+\newcommand\litCompareSafe{\textlog{lit\_compare\_safe}}
+\newcommand\valCompareSafe{\textlog{val\_compare\_safe}}
diff --git a/tex/heaplang.tex b/tex/heaplang.tex
new file mode 100644
index 0000000000000000000000000000000000000000..5bdf6e9c4e9108cd8f64b6a4c0e12369afde8cbe
--- /dev/null
+++ b/tex/heaplang.tex
@@ -0,0 +1,293 @@
+\section{HeapLang}
+\label{sec:heaplang}
+
+So far, we have treated the programming language we work on entirely generically.
+In this section we present the default language that ships with Iris, HeapLang.
+HeapLang is an ML-like languages with a higher-order heap, unstructured concurrency, some common atomic operations, and prophecy variables.
+It is an instance of the language interface (\Sref{sec:language}), so we only define a per-thread small-step operational semantics---the thread-pool semantics are given in in \Sref{sec:language:concurrent}.
+
+\subsection{HeapLang syntax and operational semantics}
+
+The grammar of HeapLang, and in particular its set \Expr{} of \emph{expressions} and \Val{} of \emph{values}, is defined as follows:
+\begin{align*}
+\val,\valB \in \Val \bnfdef{}&
+  z \mid
+  \True \mid \False \mid
+  \TT \mid
+  \poison \mid
+  \loc \mid
+  \prophid \mid {}& (z \in \integer, \loc \in \Loc, \prophid \in \ProphId) \\&
+  \RecV\lvarF(\lvar)= \expr \mid
+  (\val,\valB)_\valForm \mid
+  \Inl(\val)_\valForm \mid
+  \Inr(\val)_\valForm  \\
+\expr \in \Expr \bnfdef{}&
+  \val \mid
+  \lvar \mid
+  \RecE\lvarF(\lvar)= \expr \mid
+  \expr_1(\expr_2) \mid
+  {}\\ &
+  \HLOp_1 \expr \mid
+  \expr_1 \HLOp_2 \expr_2 \mid
+  \If \expr then \expr_1 \Else \expr_2 \mid
+  {}\\ &
+  (\expr_1,\expr_2)_\exprForm \mid
+  \Fst(\expr) \mid
+  \Snd(\expr) \mid
+  {}\\ &
+  \Inl(\expr)_\exprForm \mid
+  \Inr(\expr)_\exprForm \mid
+  \Match \expr with \Inl => \expr_1 | \Inr => \expr_2 end \mid
+  {}\\ &
+  \Alloc(\expr_1,\expr_2) \mid
+  \Free(\expr) \mid
+  \deref \expr \mid
+  \expr_1 \gets \expr_2 \mid
+  \CmpXchg(\expr_1, \expr_2, \expr_3) \mid
+  \Xchg(\expr_1, \expr_2) \mid
+  \FAA(\expr_1, \expr_2) \mid
+  \kern-30ex{}\\ &
+  \Fork \expr \mid
+  \NewProph \mid
+  \ResolveWith \expr_1 at \expr_2 to \expr_3 \\
+\HLOp_1 \bnfdef{}& - \mid \ldots ~~\text{(list incomplete)} \\
+\HLOp_2 \bnfdef{}& + \mid - \mid \Ptradd \mid \mathop{=} \mid \ldots ~~\text{(list incomplete)}
+\end{align*}
+(Note that \langkw{match} contains a literal $|$ that is not part of the BNF but part of HeapLang syntax.)
+
+To simplify the formalization, the only binders occur in \langkw{rec}.
+\langkw{match} has a closure in each arm which will be applied to the value of the left/right variant, respectively.
+(See the syntactic sugar defined later.)
+
+Recursive abstractions, pairs, and the injections exist both as a value form and an expression form.
+The expression forms will reduce to the value form once all their arguments are values.
+Conceptually, one can think of that as corresponding to ``boxing'' that most functional language implementations do.
+We will leave away the disambiguating subscript when it is clear from the context or does not matter.
+All of this lets us define $\ofval$ as simply applying the value injection (the very first syntactic form of $\Expr$), which makes a lot of things in Coq much simpler.
+$\toval$ is defined recursively in the obvious way.
+
+\langkw{Alloc} takes as first argument the number of heap cells to allocate (must be strictly positive), and as second argument the default value to use for these heap cells.
+This lets one allocate arrays.
+$\Ptradd$ implements pointer arithmetic (the left operand must be a pointer, the right operand an integer), which is used to access array elements.
+
+For our set of states and observations, we pick
+\begin{align*}
+  \loc \ni \Loc \eqdef{}& \integer \\
+  \prophid \ni \ProphId \eqdef{}& \integer \\
+  \sigma \ni \State \eqdef{}& \record{\begin{aligned}
+                   \stateHeap:{}& \Loc \fpfn \Val,\\
+                   \stateProphs:{}& \pset{\ProphId}
+                 \end{aligned}} \\
+  \obs \ni \Obs \eqdef{}& \ProphId \times (\Val \times \Val)
+\end{align*}
+
+The HeapLang operational semantics is defined via the use of \emph{evaluation contexts}:
+\begin{align*}
+\lctx \in \Lctx \bnfdef{}&
+  \bullet \mid \Lctx_{>} \\
+\lctx_{>} \in \Lctx_{>} \bnfdef{}&
+  \expr(\lctx) \mid
+  \lctx (\val) \mid
+  {}\\ &
+  \HLOp_1 \lctx \mid
+  \expr \HLOp_2 \lctx \mid
+  \lctx \HLOp_2 \val \mid
+  \If \lctx then \expr_1 \Else \expr_2 \mid
+  {}\\ &
+  (\expr, \lctx) \mid
+  (\lctx, \val) \mid
+  \Fst(\lctx) \mid
+  \Snd(\lctx) \mid
+  {}\\ &
+  \Inl(\lctx) \mid
+  \Inr(\lctx) \mid
+  \Match \lctx with \Inl => \expr_1 | \Inr => \expr_2 end \mid
+  {}\\ &
+  \Alloc(\expr, \lctx) \mid
+  \Alloc(\lctx, \val) \mid
+  \Free(\lctx) \mid
+  \deref \lctx \mid
+  \expr \gets \lctx \mid
+  \lctx \gets \val \mid
+  {}\\ &
+  \CmpXchg(\expr_1, \expr_2, \lctx) \mid
+  \CmpXchg(\expr_1, \lctx, \val_3) \mid
+  \CmpXchg(\lctx, \val_2, \val_3) \mid
+  {}\\ &
+  \Xchg(\expr, \lctx) \mid
+  \Xchg(\lctx, \val) \mid
+  \FAA(\expr, \lctx) \mid
+  \FAA(\lctx, \val) \mid
+  {}\\ &
+  \ResolveWith \expr_1 at \expr_2 to \lctx \mid
+  \ResolveWith \expr_1 at \lctx to \val_3 \mid
+  {}\\ &
+  \ResolveWith \lctx_{>} at \val_2 to \val_3
+\end{align*}
+Note that we use right-to-left evaluation order.
+This means in a curried function call $f(x)(y)$, we know syntactically the arguments will all evaluate before $f$ gets to do anything, which makes specifying curried calls a lot easier.
+
+The \langkw{resolve} evaluation context for the leftmost expression (the nested expression that executes atomically together with the prophecy resolution) is special: it must not be empty; only further nested evaluation contexts are allowed.
+\langkw{resolve} takes care of reducing the expression once the nested contexts are taken care of, and at that point it requires the expression to reduce to a value in exactly one step.
+Hence we define $\Lctx_{>}$ for non-empty evaluation contexts.
+For more details on prophecy variables, see \cite{iris:prophecy}.
+
+This lets us define the primitive reduction relation in terms of a ``head step'' reduction; see \figref{fig:heaplang-reduction-pure} and \figref{fig:heaplang-reduction-impure}.
+Comparison (both for $\CmpXchg$ and the binary comparison operator) is a bit tricky and uses a helper judgment (\figref{fig:heaplang-valeq}).
+Basically, two values can only be compared if at least one of them is ``compare-safe''.
+Compare-safe values are basic literals (integers, Booleans, locations, unit) as well as $\Inl$ and $\Inr$ of those literals.
+The intention of this is to forbid directly comparing large values such as pairs, which could not be done in a single atomic step on a real machine.
+
+\begin{figure}[p]
+\judgment[Per-thread reduction]{\expr_1, \state_1 \step [\vec\obs] \expr_2, \state_2, \vec\expr}
+\begin{mathpar}
+\infer
+  {\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+  {\fillctx\lctx[\expr_1], \state_1 \step[\vec\obs] \fillctx\lctx[\expr_2], \state_2, \vec\expr}
+\end{mathpar}
+
+\judgment[``Head'' reduction (pure)]{\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+\newcommand\alignheader{\kern-30ex}
+\begin{align*}
+&\alignheader\textbf{``Boxing'' reductions} \\
+(\RecE\lvarF(\lvar)= \expr, \state) \hstep[\nil]{}&
+  (\RecV\lvarF(\lvar)= \expr, \state, \nil) \\
+((\val_1, \val_2)_\exprForm, \state) \hstep[\nil]{}&
+  ((\val_1, \val_2)_\valForm, \state, \nil) \\
+(\Inl(\val)_\exprForm, \state) \hstep[\nil]{}&
+  (\Inl(\val)_\valForm, \state, \nil) \\
+(\Inr(\val)_\exprForm, \state) \hstep[\nil]{}&
+  (\Inr(\val)_\valForm, \state, \nil) \\
+&\alignheader\textbf{Pure reductions} \\
+((\RecV\lvarF(\lvar)= \expr)(\val), \state) \hstep[\nil]{}&
+  (\subst {\subst \expr \lvarF {(\Rec\lvarF(\lvar)= \expr)}} \lvar \val, \state, \nil) \\
+(-_{\HLOp} z, \state) \hstep[\nil]{}&
+  (-z, \state, \nil) \\
+(z_1 +_{\HLOp} z_2, \state) \hstep[\nil]{}&
+  (z_1 + z_2, \state, \nil) \\
+(z_1 -_{\HLOp} z_2, \state) \hstep[\nil]{}&
+  (z_1 - z_2, \state, \nil) \\
+(\loc \Ptradd z, \state) \hstep[\nil]{}&
+  (\loc + z, \state, \nil) \\
+(\val_1 =_{\HLOp} \val_2, \state) \hstep[\nil]{}&
+  (\True, \state, \nil)
+  &&\text{if $\val_1 \valeq \val_2$} \\
+(\val_1 =_{\HLOp} \val_2, \state) \hstep[\nil]{}&
+  (\False, \state, \nil)
+  &&\text{if $\val_1 \valne \val_2$} \\
+(\If \True then \expr_1 \Else \expr_2, \state) \hstep[\nil]{}&
+  (\expr_1, \state, \nil) \\
+(\If \False then \expr_1 \Else \expr_2, \state) \hstep[\nil]{}&
+  (\expr_2, \state, \nil) \\
+(\Fst((\val_1, \val_2)_\valForm), \state) \hstep[\nil]{}&
+  (\val_1, \state, \nil) \\
+(\Snd((\val_1, \val_2)_\valForm), \state) \hstep[\nil]{}&
+  (\val_2, \state, \nil) \\
+(\Match \Inl(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
+  (\expr_1(\val), \state, \nil) \\
+(\Match \Inr(\val)_\valForm with \Inl => \expr_1 | \Inr => \expr_2 end, \state) \hstep[\nil]{}&
+  (\expr_2(\val), \state, \nil)
+\end{align*}
+\caption{HeapLang pure and boxed reduction rules. \\ \small
+The $\HLOp$ subscript indicates that this is the HeapLang operator, not the mathematical operator.}
+\label{fig:heaplang-reduction-pure}
+\end{figure}
+
+\begin{figure}
+\judgment[``Head'' reduction (impure)]{\expr_1, \state_1 \hstep [\vec\obs] \expr_2, \state_2, \vec\expr}
+\newcommand\alignheader{\kern-30ex}
+\begin{align*}
+&\alignheader\textbf{Heap reductions} \\
+(\Alloc(z, \val), \state) \hstep[\nil]{}&
+  (\loc, \mapinsert {[\loc,\loc+z)} \val {\state:\stateHeap}, \nil)
+  &&\text{if $z>0$ and \(\All i<z. \state.\stateHeap(\loc+i) = \bot\)} \\
+(\Free(\loc), \state) \hstep[\nil]{}&
+  ((), \mapinsert \loc \bot {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\deref\loc, \state) \hstep[\nil]{}&
+  (\val, \state, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\loc\gets\valB, \state) \hstep[\nil]{}&
+  (\TT, \mapinsert \loc \valB {\state:\stateHeap}, \nil)  &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\CmpXchg(\loc,\valB_1,\valB_2), \state) \hstep[\nil]{}&
+  ((\val, \True), \mapinsert\loc{\valB_2}{\state:\stateHeap}, \nil)
+  &&\text{if $\state.\stateHeap(l) = \val$ and $\val \valeq \valB_1$} \\
+(\CmpXchg(\loc,\valB_1,\valB_2), \state) \hstep[\nil]{}&
+  ((\val, \False), \state, \nil)
+  &&\text{if $\state.\stateHeap(l) = \val$ and $\val \valne \valB_1$} \\
+(\Xchg(\loc, \valB) \hstep[\nil]{}&
+  (\val, \mapinsert \loc \valB {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = \val$} \\
+(\FAA(\loc, z_2) \hstep[\nil]{}&
+  (z_1, \mapinsert \loc {z_1+z_2} {\state:\stateHeap}, \nil) &&\text{if $\state.\stateHeap(l) = z_1$} \\
+&\alignheader\textbf{Special reductions} \\
+(\Fork\expr, \state) \hstep[\nil]{}&
+  (\TT, \state, \expr) \\
+(\NewProph, \state) \hstep[\nil]{}&
+  (\prophid, \state:\stateProphs \uplus \set{\prophid}, \nil)
+  &&\text{if $\prophid \notin \state.\stateProphs$}
+\end{align*}
+\begin{mathpar}
+\infer
+  {(\expr, \state) \hstep[\vec\obs] (\val, \state', \vec\expr')}
+  {(\ResolveWith \expr at \prophid to \valB, \state) \hstep[\vec\obs \dplus [(\prophid, (\val, \valB))]] (\val, \state', \vec\expr')}
+\end{mathpar}
+\caption{HeapLang impure reduction rules. \\ \small
+Here, $\state:\stateHeap$ denotes $\sigma$ with the $\stateHeap$ field updated as indicated.
+$[\loc,\loc+z)$ in the $\Alloc$ rule indicates that we update all locations in this (left-closed, right-open) interval.}
+\label{fig:heaplang-reduction-impure}
+\end{figure}
+
+\begin{figure}
+\judgment[Value (in)equality]{\val \valeq \valB, \val \valne \valB}
+\begin{align*}
+  \val \valeq \valB \eqdef{}& \val = \valB \land (\valCompareSafe(\val) \lor \valCompareSafe(\valB)) \\
+  \val \valne \valB \eqdef{}& \val \ne \valB \land (\valCompareSafe(\val) \lor \valCompareSafe(\valB))
+\end{align*}
+\begin{mathpar}
+  \axiom{\litCompareSafe(z)}
+
+  \axiom{\litCompareSafe(\True)}
+
+  \axiom{\litCompareSafe(\False)}
+
+  \axiom{\litCompareSafe(\loc)}
+
+  \axiom{\litCompareSafe(\TT)}
+
+\\
+
+  \infer
+    {\litCompareSafe(\val)}
+    {\valCompareSafe(\val)}
+
+  \infer
+    {\litCompareSafe(\val)}
+    {\valCompareSafe(\Inl(\val))}
+
+  \infer
+    {\litCompareSafe(\val)}
+    {\valCompareSafe(\Inr(\val))}
+\end{mathpar}
+\caption{HeapLang value comparison judgment.}
+\label{fig:heaplang-valeq}
+\end{figure}
+
+\subsection{Syntactic sugar}
+
+We recover many of the common language operations as syntactic sugar.
+\begin{align*}
+  \Lam \lvar. \expr \eqdef{}& \Rec\any(\lvar)= \expr \\
+  \Let \lvar = \expr in \expr' \eqdef{}& (\Lam \lvar. \expr')(\expr) \\
+  \expr; \expr' \eqdef{}& \Let \any = \expr in \expr' \\
+  \Skip \eqdef{}& \TT; \TT \\
+  \expr_1 \mathop{\&\&} \expr_2 \eqdef{}& \If \expr_1 then \expr_2 \Else \False \\
+  \expr_1 \mathop{||} \expr_2 \eqdef{}& \If \expr_1 then \True \Else \expr_2 \\
+  \Match \expr with \Inl(\lvar) => \expr_1 | \Inr(\lvarB) => \expr_2 end \eqdef {}&
+    \Match \expr with \Inl => \Lam\lvar. \expr_1 | \Inr => \Lam\lvarB. \expr_2 end \\
+  \Ref(\expr) \eqdef{}& \Alloc(1,\expr) \\
+  \CAS(\expr_1, \expr_2, \expr_3) \eqdef{}& \Snd(\CmpXchg(\expr_1, \expr_2, \expr_3)) \\
+  \Resolve \expr_1 to \expr_2 \eqdef{}& \ResolveWith \Skip at \expr_1 to \expr_2
+\end{align*}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "iris"
+%%% End:
diff --git a/tex/iris.sty b/tex/iris.sty
index fc371567ba378b616c7fb4e6f82daf74846ffccf..2eae486b47c8b4496ed08ba80824de14bd994dbe 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -31,6 +31,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \newcommand{\nat}{\mathbb{N}}
+\newcommand{\integer}{\mathbb{Z}}
 
 \DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}} % big-star
 \newcommand*{\disj}[1][]{\mathrel{\#_{#1}}}
diff --git a/tex/iris.tex b/tex/iris.tex
index 0895f76fb14727e55f476efee5cc833807497b12..0631f53daa8bd12331c635e23b74c7d226c1aae5 100644
--- a/tex/iris.tex
+++ b/tex/iris.tex
@@ -27,7 +27,7 @@
 This document describes formally the Iris program logic.
 Every result in this document has been fully verified in Coq.
 The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/iris/iris}.
-For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
+For further information, visit the Iris project website at \url{https://iris-project.org}.
 \end{abstract}
 
 \clearpage\begingroup
@@ -69,6 +69,9 @@ For a list of changes in Iris since then, please consult our changelog at \url{h
 \input{paradoxes}
 \endgroup
 \clearpage\begingroup
+\input{heaplang}
+\endgroup
+\clearpage\begingroup
 \printbibliography
 \endgroup
 
diff --git a/tex/language.tex b/tex/language.tex
index 88c6e927587b9fa57f0a4c6f9094f3e05ef475f6..4096960c4be09566de402b8fec9d4e7688316901 100644
--- a/tex/language.tex
+++ b/tex/language.tex
@@ -46,6 +46,7 @@ Otherwise, we need strong atomicity.
 \end{defn}
 
 \subsection{Concurrent Language}
+\label{sec:language:concurrent}
 
 For any language $\Lang$, we define the corresponding thread-pool semantics.
 
diff --git a/tex/setup.tex b/tex/setup.tex
index f7b3d1b097f7317ab13e3a6e7fa7e613a94ca3de..3a3bc63cebb9832e75e31ca32d353b7df92fd498 100644
--- a/tex/setup.tex
+++ b/tex/setup.tex
@@ -18,6 +18,7 @@
 
 \usepackage{\basedir pftools}
 \usepackage{\basedir iris}
+\usepackage{\basedir heaplang}
 
 \usepackage{xcolor}  % for print version