diff --git a/semantics.opam b/semantics.opam
index fe4d8e489b87cdaa5c090ccf7689bd4f89c10456..41493c33f2a3c926067840b37cc9ae1286c61157 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
 
 depends: [
   "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
-  "coq-iris-heap-lang" { (= "dev.2023-10-03.0.70b30af7") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2024-06-10.0.84ed8993") | (= "dev") }
   "coq-equations" { (= "1.3+8.18") }
   "coq-autosubst" { (= "1.8") | (= "dev")  }
 ]
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index e31f12fa73b31e178746a922b1dc143bb0932e6f..5d766c664c2538d1dbac41f4e06442410c729ea1 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -26,13 +26,13 @@ Global Instance heapGS_irisGS `{!heapGS Σ} : irisGS heap_lang Σ := {
 the notations.  That also helps for scopes and coercions. *)
 (** FIXME: Refactor these notations using custom entries once Coq bug #13654
 has been fixed. *)
-Notation "l ↦{ dq } v" := (mapsto (L:=loc) (V:=option val) l dq (Some v%V))
+Notation "l ↦{ dq } v" := (pointsto (L:=loc) (V:=option val) l dq (Some v%V))
   (at level 20, format "l  ↦{ dq }  v") : bi_scope.
-Notation "l ↦□ v" := (mapsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
+Notation "l ↦□ v" := (pointsto (L:=loc) (V:=option val) l DfracDiscarded (Some v%V))
   (at level 20, format "l  ↦□  v") : bi_scope.
-Notation "l ↦{# q } v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
+Notation "l ↦{# q } v" := (pointsto (L:=loc) (V:=option val) l (DfracOwn q) (Some v%V))
   (at level 20, format "l  ↦{# q }  v") : bi_scope.
-Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
+Notation "l ↦ v" := (pointsto (L:=loc) (V:=option val) l (DfracOwn 1) (Some v%V))
   (at level 20, format "l  ↦  v") : bi_scope.
 
 Section lifting.
@@ -63,35 +63,35 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
-Proof. apply mapsto_valid. Qed.
-Lemma mapsto_valid_2 l dq1 dq2 v1 v2 :
+Lemma pointsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
+Proof. apply pointsto_valid. Qed.
+Lemma pointsto_valid_2 l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
 Proof.
-  iIntros "H1 H2". 
-  iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=]]. done.
+  iIntros "H1 H2".
+  iDestruct (pointsto_valid_2 with "H1 H2") as %[? [=]]. done.
 Qed.
-Lemma mapsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=]. done. Qed.
+Lemma pointsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
+Proof. iIntros "H1 H2". iDestruct (pointsto_agree with "H1 H2") as %[=]. done. Qed.
 
-Lemma mapsto_combine l dq1 dq2 v1 v2 :
+Lemma pointsto_combine l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
 Proof.
-  iIntros "Hl1 Hl2". iDestruct (mapsto_combine with "Hl1 Hl2") as "[$ Heq]".
+  iIntros "Hl1 Hl2". iDestruct (pointsto_combine with "Hl1 Hl2") as "[$ Heq]".
   by iDestruct "Heq" as %[= ->].
 Qed.
 
-Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+Lemma pointsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
   ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply mapsto_frac_ne. Qed.
-Lemma mapsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply mapsto_ne. Qed.
+Proof. apply pointsto_frac_ne. Qed.
+Lemma pointsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+Proof. apply pointsto_ne. Qed.
 
-Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
-Proof. apply mapsto_persist. Qed.
+Lemma pointsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
+Proof. apply pointsto_persist. Qed.
 
-Lemma heap_array_to_seq_mapsto l v (n : nat) :
-  ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.mapsto l' (DfracOwn 1) ov) -∗
+Lemma heap_array_to_seq_pointsto l v (n : nat) :
+  ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.pointsto l' (DfracOwn 1) ov) -∗
   [∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
 Proof.
   iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
@@ -112,9 +112,9 @@ Lemma wp_allocN_seq s E v n Φ :
   WP AllocN (Val $ LitV $ LitInt $ n) (Val v) @ s; E; E {{ Φ }}.
 Proof.
   iIntros (Hn) "HΦ".
-  iApply wp_lift_head_step_fupd_nomask; first done.
-  iIntros (σ1) "Hσ !>"; iSplit; first by destruct n; auto with lia head_step.
-  iIntros (e2 σ2 κ efs Hstep); inv_head_step.
+  iApply wp_lift_base_step_fupd_nomask; first done.
+  iIntros (σ1) "Hσ !>"; iSplit; first by destruct n; auto with lia base_step.
+  iIntros (e2 σ2 κ efs Hstep); inv_base_step.
   iMod (gen_heap_alloc_big _ (heap_array _ (replicate (Z.to_nat n) v)) with "Hσ")
     as "(Hσ & Hl & Hm)".
   { apply heap_array_map_disjoint.
@@ -122,7 +122,7 @@ Proof.
   iApply step_fupd_intro; first done.
   iModIntro. iFrame "Hσ". do 2 (iSplit; first done).
   iApply wp_value_fupd. iApply "HΦ".
-  by iApply heap_array_to_seq_mapsto.
+  by iApply heap_array_to_seq_pointsto.
 Qed.
 
 Lemma wp_alloc s E v Φ :
@@ -138,10 +138,10 @@ Lemma wp_free s E l v Φ :
   (▷ Φ (LitV LitUnit)) -∗
   WP Free (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
 Proof.
-  iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
+  iIntros ">Hl HΦ". iApply wp_lift_base_step_fupd_nomask; first done.
   iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto with head_step.
-  iIntros (e2 σ2 κ efs Hstep); inv_head_step.
+  iSplit; first by eauto with base_step.
+  iIntros (e2 σ2 κ efs Hstep); inv_base_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iIntros "!>!>!>". iSplit; first done. iSplit; first done.
   iApply wp_value. by iApply "HΦ".
@@ -152,10 +152,10 @@ Lemma wp_load s E l dq v Φ :
   ▷ (l ↦{dq} v -∗ Φ v) -∗
   WP Load (Val $ LitV $ LitLoc l) @ s; E; E {{ Φ }}.
 Proof.
-  iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
+  iIntros ">Hl HΦ". iApply wp_lift_base_step_fupd_nomask; first done.
   iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto with head_step.
-  iIntros (e2 σ2 κ efs Hstep); inv_head_step.
+  iSplit; first by eauto with base_step.
+  iIntros (e2 σ2 κ efs Hstep); inv_base_step.
   iApply step_fupd_intro; first done. iNext. iFrame.
   iSplitR; first done. iSplitR; first done. iApply wp_value. by iApply "HΦ".
 Qed.
@@ -165,10 +165,10 @@ Lemma wp_store s E l v' v Φ :
   ▷ (l ↦ v -∗ Φ (LitV LitUnit)) -∗
   WP Store (Val $ LitV $ LitLoc l) (Val v) @ s; E; E {{ Φ }}.
 Proof.
-  iIntros ">Hl HΦ". iApply wp_lift_head_step_fupd_nomask; first done.
+  iIntros ">Hl HΦ". iApply wp_lift_base_step_fupd_nomask; first done.
   iIntros (σ1) "Hσ !>". iDestruct (gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto with head_step.
-  iIntros (e2 σ2 κ efs Hstep); inv_head_step.
+  iSplit; first by eauto with base_step.
+  iIntros (e2 σ2 κ efs Hstep); inv_base_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iApply step_fupd_intro; first done. iNext.
   iSplit; first done. iSplit; first done.
diff --git a/theories/program_logics/hoare_lib.v b/theories/program_logics/hoare_lib.v
index aa204910e376d7092aa2f4ddce2f44a824e493ac..10ce03ffac819defd9070e115fddb1a6468e8a80 100644
--- a/theories/program_logics/hoare_lib.v
+++ b/theories/program_logics/hoare_lib.v
@@ -149,7 +149,7 @@ Module hoare.
     l ↦ v ∗ l ↦ w ⊢ False.
   Proof.
     iIntros "[Ha Hb]".
-    iPoseProof (mapsto_ne with "Ha Hb") as "%Hneq".
+    iPoseProof (pointsto_ne with "Ha Hb") as "%Hneq".
     done.
   Qed.
 
diff --git a/theories/program_logics/program_logic/ectx_lifting.v b/theories/program_logics/program_logic/ectx_lifting.v
index b05640ff5ad5b4f1758df5ae201b5a3e5f8796cf..071d26a5f2fe1d23f88f2120974d2f904a52fc99 100644
--- a/theories/program_logics/program_logic/ectx_lifting.v
+++ b/theories/program_logics/program_logic/ectx_lifting.v
@@ -11,16 +11,16 @@ Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
-Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
+Local Hint Resolve base_prim_reducible base_reducible_prim_step : core.
 Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
 Local Hint Resolve reducible_not_val_inhabitant : core.
-Local Hint Resolve head_stuck_stuck : core.
+Local Hint Resolve base_stuck_stuck : core.
 
-Lemma wp_lift_head_step_fupd {s E1 E2 Φ} e1 :
+Lemma wp_lift_base_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (|={E1, ∅}=> ∀ σ1, state_interp σ1 ={∅,∅}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 κ efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅}=>
+    ⌜base_reducible e1 σ1⌝ ∗
+    ∀ e2 σ2 κ efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗ ▷ |={∅}=>
       state_interp σ2 ∗ ⌜efs = []⌝ ∗ ⌜κ = []⌝ ∗
       WP e2 @ s; ∅; E2 {{ Φ }})
   ⊢ WP e1 @ s; E1; E2 {{ Φ }}.
@@ -32,24 +32,24 @@ Proof.
   iIntros "($ & $ & $)".
 Qed.
 
-Lemma wp_lift_head_step {s E1 E2 Φ} e1 :
+Lemma wp_lift_base_step {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (|={E1, ∅}=> ∀ σ1, state_interp σ1 ={∅}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ▷ ∀ e2 σ2 κ efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗
+    ⌜base_reducible e1 σ1⌝ ∗
+    ▷ ∀ e2 σ2 κ efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={∅}=∗
       state_interp σ2 ∗ ⌜efs = []⌝ ∗ ⌜κ = []⌝ ∗ WP e2 @ s; ∅; E2 {{ Φ }})
   ⊢ WP e1 @ s; E1; E2 {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iMod "H".
+  iIntros (?) "H". iApply wp_lift_base_step_fupd; [done|]. iMod "H".
   iIntros "!>" (?) "?".
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 κ efs ?) "!> !>". by iApply "H".
 Qed.
 
-Lemma wp_lift_head_step_fupd_nomask {s E1 E2 E3 Φ} e1 :
+Lemma wp_lift_base_step_fupd_nomask {s E1 E2 E3 Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E1}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 κ efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E3]▷=∗
+    ⌜base_reducible e1 σ1⌝ ∗
+    ∀ e2 σ2 κ efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E3]▷=∗
       state_interp σ2 ∗ ⌜efs = []⌝ ∗ ⌜κ = []⌝ ∗
       WP e2 @ s; E1; E2 {{ Φ }})
   ⊢ WP e1 @ s; E1; E2 {{ Φ }}.
@@ -61,25 +61,25 @@ Proof.
   iIntros "($ & $)".
 Qed.
 
-Lemma wp_lift_pure_det_head_step {s E1 E2 E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_base_step {s E1 E2 E' Φ} e1 e2 :
   to_val e1 = None →
-  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1, base_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
+    base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
   (|={E1}[E']▷=> WP e2 @ s; E1; E2 {{ Φ }}) ⊢ WP e1 @ s; E1; E2 {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2); eauto.
   destruct s; by auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step' {s E1 E2 Φ} e1 e2 :
+Lemma wp_lift_pure_det_base_step' {s E1 E2 Φ} e1 e2 :
   to_val e1 = None →
-  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1, base_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
+    base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
   ▷ WP e2 @ s; E1; E2 {{ Φ }} ⊢ WP e1 @ s; E1; E2 {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step //.
+  intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_base_step //.
   rewrite -step_fupd_intro //.
 Qed.
 End wp.
diff --git a/theories/program_logics/reloc/src_rules.v b/theories/program_logics/reloc/src_rules.v
index abada6393b1bfdcafedb07499aa5f87973395554..0616302d5a3886ff0ac62427a3487eb50133dadf 100644
--- a/theories/program_logics/reloc/src_rules.v
+++ b/theories/program_logics/reloc/src_rules.v
@@ -187,7 +187,7 @@ Section rules.
   (** For the following execution lemmas, you will find the following lemmas helpful:
     - prim_thread_step
     - fill_prim_step
-    - head_prim_step
+    - base_prim_step
   *)
 
   Lemma src_step_load E K l v :