diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 76e077e5552fb64eeb9f6c801287bb667a5fbe59..24b5b63346f4f30e78363ace8f922bd916cea842 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -109,6 +109,7 @@ Inductive expr :=
   | Fork (e : expr)
   (* Heap *)
   | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
+  | Free (e : expr)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CmpXchg (e0 : expr) (e1 : expr) (e2 : expr) (* Compare-exchange *)
@@ -242,6 +243,8 @@ Proof.
      | 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' =>
+        cast_if (decide (e = e'))
      | Load e, Load e' => cast_if (decide (e = e'))
      | Store e1 e2, Store e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
@@ -325,12 +328,13 @@ Proof.
      | Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
      | Fork e => GenNode 12 [go e]
      | AllocN e1 e2 => GenNode 13 [go e1; go e2]
-     | Load e => GenNode 14 [go e]
-     | Store e1 e2 => GenNode 15 [go e1; go e2]
-     | CmpXchg e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
-     | FAA e1 e2 => GenNode 17 [go e1; go e2]
-     | NewProph => GenNode 18 []
-     | Resolve e0 e1 e2 => GenNode 19 [go e0; go e1; go e2]
+     | Free e => GenNode 14 [go e]
+     | Load e => GenNode 15 [go e]
+     | Store e1 e2 => GenNode 16 [go e1; go e2]
+     | CmpXchg e0 e1 e2 => GenNode 17 [go e0; go e1; go e2]
+     | FAA e1 e2 => GenNode 18 [go e1; go e2]
+     | NewProph => GenNode 19 []
+     | Resolve e0 e1 e2 => GenNode 20 [go e0; go e1; go e2]
      end
    with gov v :=
      match v with
@@ -360,12 +364,13 @@ Proof.
      | GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
      | GenNode 12 [e] => Fork (go e)
      | GenNode 13 [e1; e2] => AllocN (go e1) (go e2)
-     | GenNode 14 [e] => Load (go e)
-     | GenNode 15 [e1; e2] => Store (go e1) (go e2)
-     | GenNode 16 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
-     | GenNode 17 [e1; e2] => FAA (go e1) (go e2)
-     | GenNode 18 [] => NewProph
-     | GenNode 19 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
+     | GenNode 14 [e] => Free (go e)
+     | GenNode 15 [e] => Load (go e)
+     | GenNode 16 [e1; e2] => Store (go e1) (go e2)
+     | GenNode 17 [e0; e1; e2] => CmpXchg (go e0) (go e1) (go e2)
+     | GenNode 18 [e1; e2] => FAA (go e1) (go e2)
+     | GenNode 19 [] => NewProph
+     | GenNode 20 [e0; e1; e2] => Resolve (go e0) (go e1) (go e2)
      | _ => Val $ LitV LitUnit (* dummy *)
      end
    with gov v :=
@@ -380,7 +385,7 @@ Proof.
    for go).
  refine (inj_countable' enc dec _).
  refine (fix go (e : expr) {struct e} := _ with gov (v : val) {struct v} := _ for go).
- - destruct e as [v| | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
+ - destruct e as [v| | | | | | | | | | | | | | | | | | | | |]; simpl; f_equal;
      [exact (gov v)|done..].
  - destruct v; by f_equal.
 Qed.
@@ -414,6 +419,7 @@ Inductive ectx_item :=
   | CaseCtx (e1 : expr) (e2 : expr)
   | AllocNLCtx (v2 : val)
   | AllocNRCtx (e1 : expr)
+  | FreeCtx
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
@@ -450,6 +456,7 @@ Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
   | CaseCtx e1 e2 => Case e e1 e2
   | AllocNLCtx v2 => AllocN e (Val v2)
   | AllocNRCtx e1 => AllocN e1 e
+  | FreeCtx => Free e
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
@@ -482,6 +489,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | 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)
   | 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)
@@ -650,6 +658,12 @@ Inductive head_step : expr → state → list observation → expr → state →
                []
                (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
                []
+  | FreeS l v σ :
+     σ.(heap) !! l = Some $ Some v →
+     head_step (Free (Val $ LitV $ LitLoc l)) σ
+               []
+               (Val $ LitV LitUnit) (state_upd_heap <[l:=None]> σ)
+               []
   | LoadS l v σ :
      σ.(heap) !! l = Some $ Some v →
      head_step (Load (Val $ LitV $ LitLoc l)) σ [] (of_val v) σ []
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index 51077ca0dbfbabe1d74d0c2a73c64800692def23..0859f72697bf77ceb005cfa330cc3431dc39d39a 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -10,7 +10,7 @@ Fixpoint is_closed_expr (X : list string) (e : expr) : bool :=
   | Val v => is_closed_val v
   | Var x => bool_decide (x ∈ X)
   | Rec f x e => is_closed_expr (f :b: x :b: X) e
-  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Free e | Load e =>
      is_closed_expr X e
   | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
@@ -156,6 +156,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | Fork e => Fork (subst_map vs e)
   | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
+  | Free e => Free (subst_map vs e)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
   | CmpXchg e0 e1 e2 => CmpXchg (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v
index d4f8ca3f0d2c0bd2aa7c6b38bc2723aeb4766c43..ca5671830b9c4ee7e80cfa383c4266d50a99de73 100644
--- a/theories/heap_lang/proph_erasure.v
+++ b/theories/heap_lang/proph_erasure.v
@@ -40,6 +40,7 @@ Fixpoint erase_expr (e : expr) : expr :=
   | Case e0 e1 e2 => Case (erase_expr e0) (erase_expr e1) (erase_expr e2)
   | Fork e => Fork (erase_expr e)
   | AllocN e1 e2 => AllocN (erase_expr e1) (erase_expr e2)
+  | Free e => Free (erase_expr e)
   | Load e => Load (erase_expr e)
   | Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
   | CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
@@ -93,6 +94,7 @@ Fixpoint erase_ectx_item (Ki : ectx_item) : list ectx_item :=
   | CaseCtx e1 e2 => [CaseCtx (erase_expr e1) (erase_expr e2)]
   | AllocNLCtx v2 => [AllocNLCtx (erase_val v2)]
   | AllocNRCtx e1 => [AllocNRCtx (erase_expr e1)]
+  | FreeCtx => [FreeCtx]
   | LoadCtx => [LoadCtx]
   | StoreLCtx v2 => [StoreLCtx (erase_val v2)]
   | StoreRCtx e1 => [StoreRCtx (erase_expr e1)]
@@ -193,11 +195,16 @@ Proof. rewrite lookup_fmap; by destruct (h !! l). Qed.
 Lemma lookup_erase_heap h l : erase_heap h !! l = (λ ov, erase_val <$> ov) <$> h !! l.
 Proof. by rewrite lookup_fmap. Qed.
 
-Lemma erase_heap_insert h l v :
+Lemma erase_heap_insert_Some h l v :
   erase_heap (<[l := Some v]> h) = <[l := Some $ erase_val v]> (erase_heap h).
 Proof.
   by rewrite /erase_heap fmap_insert.
 Qed.
+Lemma erase_heap_insert_None h l v :
+  erase_heap (<[l := None]> h) = <[l := None]> (erase_heap h).
+Proof.
+  by rewrite /erase_heap fmap_insert.
+Qed.
 
 Lemma fmap_heap_array (f : val → val) l vs :
   (λ ov : option val, f <$> ov) <$> heap_array l vs = heap_array l (f <$> vs).
@@ -247,6 +254,17 @@ Proof.
     first econstructor; try setoid_rewrite <- lookup_erase_heap_None;
       rewrite ?erase_heap_insert /=; eauto using erase_state_init.
 Qed.
+Lemma erased_head_step_head_step_Free l v σ :
+  erase_heap (heap σ) !! l = Some (Some v) →
+  head_steps_to_erasure_of (Free #l) σ #()
+   {| heap := <[l:=None]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
+Proof.
+  intros Hl.
+  rewrite lookup_erase_heap in Hl.
+  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
+  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
+  rewrite /state_upd_heap /erase_state /= erase_heap_insert_None //.
+Qed.
 Lemma erased_head_step_head_step_Load l σ v :
   erase_heap (heap σ) !! l = Some (Some v) →
   head_steps_to_erasure_of (! #l) σ v (erase_state σ) [].
@@ -256,7 +274,6 @@ Proof.
   destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
   eexists _, _, _, _; simpl; split; first econstructor; eauto.
 Qed.
-
 Lemma erased_head_step_head_step_Store l v w σ :
   erase_heap (heap σ) !! l = Some (Some v) →
   head_steps_to_erasure_of (#l <- w) σ #()
@@ -266,7 +283,7 @@ Proof.
   rewrite lookup_erase_heap in Hl.
   destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
   eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
-    by rewrite /state_upd_heap /erase_state /= erase_heap_insert.
+  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
 Qed.
 Lemma erased_head_step_head_step_CmpXchg l v w σ vl :
   erase_heap (heap σ) !! l = Some (Some vl) →
@@ -287,7 +304,7 @@ Proof.
   - eexists _, _, _, _; simpl; split.
     { econstructor; eauto. }
     rewrite !bool_decide_eq_true_2; eauto using erase_val_inj_iff; [].
-    rewrite -?erase_heap_insert.
+    rewrite -?erase_heap_insert_Some.
     split_and!; auto.
   - eexists _, _, _, _; simpl; split.
     { econstructor; eauto. }
@@ -305,7 +322,7 @@ Proof.
   rewrite lookup_erase_heap in Hl.
   destruct (heap σ !! l) as [[[[]| | | |]|]|] eqn:?; simplify_eq/=.
   repeat econstructor; first by eauto.
-  by rewrite /state_upd_heap /erase_state /= erase_heap_insert.
+  by rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some.
 Qed.
 
 (** When the erased program makes a head step, so does the original program. *)
@@ -329,6 +346,7 @@ Proof.
   eauto using erased_head_step_head_step_rec,
     erased_head_step_head_step_NewProph,
     erased_head_step_head_step_AllocN,
+    erased_head_step_head_step_Free,
     erased_head_step_head_step_Load,
     erased_head_step_head_step_Store,
     erased_head_step_head_step_CmpXchg,
@@ -667,6 +685,14 @@ Proof.
   intros; rewrite lookup_erase_heap_None; eauto.
 Qed.
 
+Lemma head_step_erased_prim_step_free σ l v :
+  heap σ !! l = Some (Some v) →
+  ∃ e2' σ2' ef', prim_step (Free #l) (erase_state σ) [] e2' σ2' ef'.
+Proof.
+  intros Hw. do 3 eexists; apply head_prim_step; econstructor.
+  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
+Qed.
+
 Lemma head_step_erased_prim_step_load σ l v:
   heap σ !! l = Some (Some v) →
   ∃ e2' σ2' ef', prim_step (! #l) (erase_state σ) [] e2' σ2' ef'.
@@ -708,6 +734,7 @@ Proof.
                 head_step_erased_prim_step_un_op,
                 head_step_erased_prim_step_bin_op,
                 head_step_erased_prim_step_allocN,
+                head_step_erased_prim_step_free,
                 head_step_erased_prim_step_load,
                 head_step_erased_prim_step_store,
                 head_step_erased_prim_step_FAA;
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 368f202fe40127e70e64b10c6bf0bf755bef4cab..c3325b8dd09014e4bd41247f0d138379b93c37b7 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -32,6 +32,7 @@ Ltac reshape_expr e tac :=
     | Case ?e0 ?e1 ?e2                => add_item (CaseCtx e1 e2) vs K e0
     | AllocN ?e (Val ?v)              => add_item (AllocNLCtx v) vs K e
     | AllocN ?e1 ?e2                  => add_item (AllocNRCtx e1) vs K e2
+    | Free ?e                         => add_item FreeCtx vs K e
     | Load ?e                         => add_item LoadCtx vs K e
     | Store ?e (Val ?v)               => add_item (StoreLCtx v) vs K e
     | Store ?e1 ?e2                   => add_item (StoreRCtx e1) vs K e2