diff --git a/_CoqProject b/_CoqProject
index 3a2479f514cb962bfcb09879c9f50cbf152671a5..e88b58a5b3e784c1a2d73725871548ce19b324e8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -91,6 +91,7 @@ theories/program_logic/ownp.v
 theories/program_logic/total_lifting.v
 theories/program_logic/total_ectx_lifting.v
 theories/program_logic/atomic.v
+theories/heap_lang/locations.v
 theories/heap_lang/lang.v
 theories/heap_lang/metatheory.v
 theories/heap_lang/tactics.v
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 041b177baa2ca907e531981444618d26fc84b3ca..ebde315ef532338106d2e92fd940d5ec72464eaf 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -144,6 +144,16 @@ Section tests.
     WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
   Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
 
+  Lemma wp_alloc_array n : 0 < n →
+    {{{ True }}}
+      AllocN #n #0
+    {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}%I.
+  Proof.
+    iIntros (? ?) "!# _ HΦ".
+    wp_alloc l as "?"; first done.
+    by iApply "HΦ".
+  Qed.
+
 End tests.
 
 Section printing_tests.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 13502ff5e410e602edceb142de41d54e7db804c8..50b2f7310e43423dcfc658376f171dbd8ac13cf0 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -142,6 +142,22 @@ Section gen_heap.
     iModIntro. rewrite to_gen_heap_insert. iFrame.
   Qed.
 
+  Lemma gen_heap_alloc_gen σ σ' :
+    σ ##ₘ σ' → gen_heap_ctx σ ==∗ gen_heap_ctx (σ ∪ σ') ∗ [∗ map] l ↦ v ∈ σ', l ↦ v.
+  Proof.
+    revert σ; induction σ' as [| l v σ' Hl IHσ'] using map_ind;
+      iIntros (σ Hσdisj) "Hσ".
+    - by rewrite right_id big_opM_empty; iFrame.
+    - iMod (IHσ' with "Hσ") as "[Hσ m]"; first by eapply map_disjoint_insert_r.
+      rewrite big_opM_insert //; iFrame.
+      assert (σ !! l = None).
+      { eapply map_disjoint_Some_r; first by eauto.
+        rewrite lookup_insert //. }
+      rewrite -insert_union_r //.
+      iMod (gen_heap_alloc with "Hσ") as "[$ $]"; last done.
+      apply lookup_union_None; split; auto.
+  Qed.
+
   Lemma gen_heap_dealloc σ l v :
     gen_heap_ctx σ -∗ l ↦ v ==∗ gen_heap_ctx (delete l σ).
   Proof.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e1585242f58a882222d2b342dd582c94347e085c..9edced2d4ae526a2ddcf74f5a9071049affe9658 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
+From iris.heap_lang Require Export locations.
 From iris.algebra Require Export ofe.
 From stdpp Require Export binders strings.
 From stdpp Require Import gmap.
@@ -28,7 +29,6 @@ Module heap_lang.
 Open Scope Z_scope.
 
 (** Expressions and vals. *)
-Definition loc := positive. (* Really, any countable type. *)
 Definition proph_id := positive.
 
 Inductive base_lit : Set :=
@@ -40,7 +40,8 @@ Inductive bin_op : Set :=
   | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
   | AndOp | OrOp | XorOp (* Bitwise *)
   | ShiftLOp | ShiftROp (* Shifts *)
-  | LeOp | LtOp | EqOp. (* Relations *)
+  | LeOp | LtOp | EqOp (* Relations *)
+  | OffsetOp. (* Pointer offset *)
 
 Inductive expr :=
   (* Values *)
@@ -64,7 +65,7 @@ Inductive expr :=
   (* Concurrency *)
   | Fork (e : expr)
   (* Heap *)
-  | Alloc (e : expr)
+  | AllocN (e1 e2 : expr) (* array length (positive number), initial value *)
   | Load (e : expr)
   | Store (e1 : expr) (e2 : expr)
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
@@ -170,7 +171,8 @@ Proof.
      | 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'))
-     | Alloc e, Alloc e' => cast_if (decide (e = e'))
+     | AllocN e1 e2, AllocN e1' e2' =>
+        cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
      | Load e, Load e' => cast_if (decide (e = e'))
      | Store e1 e2, Store e1' e2' =>
         cast_if_and (decide (e1 = e1')) (decide (e2 = e2'))
@@ -221,11 +223,11 @@ Proof.
  refine (inj_countable' (λ op, match op with
   | PlusOp => 0 | MinusOp => 1 | MultOp => 2 | QuotOp => 3 | RemOp => 4
   | AndOp => 5 | OrOp => 6 | XorOp => 7 | ShiftLOp => 8 | ShiftROp => 9
-  | LeOp => 10 | LtOp => 11 | EqOp => 12
+  | LeOp => 10 | LtOp => 11 | EqOp => 12 | OffsetOp => 13
   end) (λ n, match n with
   | 0 => PlusOp | 1 => MinusOp | 2 => MultOp | 3 => QuotOp | 4 => RemOp
   | 5 => AndOp | 6 => OrOp | 7 => XorOp | 8 => ShiftLOp | 9 => ShiftROp
-  | 10 => LeOp | 11 => LtOp | _ => EqOp
+  | 10 => LeOp | 11 => LtOp | 12 => EqOp | _ => OffsetOp
   end) _); by intros [].
 Qed.
 Instance expr_countable : Countable expr.
@@ -247,7 +249,7 @@ Proof.
      | InjR e => GenNode 10 [go e]
      | Case e0 e1 e2 => GenNode 11 [go e0; go e1; go e2]
      | Fork e => GenNode 12 [go e]
-     | Alloc e => GenNode 13 [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]
      | CAS e0 e1 e2 => GenNode 16 [go e0; go e1; go e2]
@@ -282,7 +284,7 @@ Proof.
      | GenNode 10 [e] => InjR (go e)
      | GenNode 11 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
      | GenNode 12 [e] => Fork (go e)
-     | GenNode 13 [e] => Alloc (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] => CAS (go e0) (go e1) (go e2)
@@ -335,7 +337,8 @@ Inductive ectx_item :=
   | InjLCtx
   | InjRCtx
   | CaseCtx (e1 : expr) (e2 : expr)
-  | AllocCtx
+  | AllocNLCtx (v2 : val)
+  | AllocNRCtx (e1 : expr)
   | LoadCtx
   | StoreLCtx (v2 : val)
   | StoreRCtx (e1 : expr)
@@ -362,7 +365,8 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | InjLCtx => InjL e
   | InjRCtx => InjR e
   | CaseCtx e1 e2 => Case e e1 e2
-  | AllocCtx => Alloc e
+  | AllocNLCtx v2 => AllocN e (Val v2)
+  | AllocNRCtx e1 => AllocN e1 e
   | LoadCtx => Load e
   | StoreLCtx v2 => Store e (Val v2)
   | StoreRCtx e1 => Store e1 e
@@ -393,7 +397,7 @@ Fixpoint subst (x : string) (v : val) (e : expr)  : expr :=
   | 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)
-  | Alloc e => Alloc (subst x v e)
+  | AllocN e1 e2 => AllocN (subst x v e1) (subst x v e2)
   | Load e => Load (subst x v e)
   | Store e1 e2 => Store (subst x v e1) (subst x v e2)
   | CAS e0 e1 e2 => CAS (subst x v e0) (subst x v e1) (subst x v e2)
@@ -414,21 +418,22 @@ Definition un_op_eval (op : un_op) (v : val) : option val :=
   | _, _ => None
   end.
 
-Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : base_lit :=
+Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : option base_lit :=
   match op with
-  | PlusOp => LitInt (n1 + n2)
-  | MinusOp => LitInt (n1 - n2)
-  | MultOp => LitInt (n1 * n2)
-  | QuotOp => LitInt (n1 `quot` n2)
-  | RemOp => LitInt (n1 `rem` n2)
-  | AndOp => LitInt (Z.land n1 n2)
-  | OrOp => LitInt (Z.lor n1 n2)
-  | XorOp => LitInt (Z.lxor n1 n2)
-  | ShiftLOp => LitInt (n1 ≪ n2)
-  | ShiftROp => LitInt (n1 ≫ n2)
-  | LeOp => LitBool (bool_decide (n1 ≤ n2))
-  | LtOp => LitBool (bool_decide (n1 < n2))
-  | EqOp => LitBool (bool_decide (n1 = n2))
+  | PlusOp => Some $ LitInt (n1 + n2)
+  | MinusOp => Some $ LitInt (n1 - n2)
+  | MultOp => Some $ LitInt (n1 * n2)
+  | QuotOp => Some $ LitInt (n1 `quot` n2)
+  | RemOp => Some $ LitInt (n1 `rem` n2)
+  | AndOp => Some $ LitInt (Z.land n1 n2)
+  | OrOp => Some $ LitInt (Z.lor n1 n2)
+  | XorOp => Some $ LitInt (Z.lxor n1 n2)
+  | ShiftLOp => Some $ LitInt (n1 ≪ n2)
+  | ShiftROp => Some $ LitInt (n1 ≫ n2)
+  | LeOp => Some $ LitBool (bool_decide (n1 ≤ n2))
+  | LtOp => Some $ LitBool (bool_decide (n1 < n2))
+  | EqOp => Some $ LitBool (bool_decide (n1 = n2))
+  | OffsetOp => None (* Pointer arithmetic *)
   end.
 
 Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
@@ -440,13 +445,15 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
   | ShiftLOp | ShiftROp => None (* Shifts *)
   | LeOp | LtOp => None (* InEquality *)
   | EqOp => Some (LitBool (bool_decide (b1 = b2)))
+  | OffsetOp => None (* Pointer arithmetic *)
   end.
 
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
   if decide (op = EqOp) then Some $ LitV $ LitBool $ bool_decide (v1 = v2) else
   match v1, v2 with
-  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
+  | LitV (LitInt n1), LitV (LitInt n2) => LitV <$> bin_op_eval_int op n1 n2
   | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
+  | LitV (LitLoc l), LitV (LitInt off) => Some $ LitV $ LitLoc (l +â‚— off)
   | _, _ => None
   end.
 
@@ -461,10 +468,53 @@ Arguments vals_cas_compare_safe !_ !_ /.
 Definition state_upd_heap (f: gmap loc val → gmap loc val) (σ: state) : state :=
   {| heap := f σ.(heap); used_proph_id := σ.(used_proph_id) |}.
 Arguments state_upd_heap _ !_ /.
+
 Definition state_upd_used_proph_id (f: gset proph_id → gset proph_id) (σ: state) : state :=
   {| heap := σ.(heap); used_proph_id := f σ.(used_proph_id) |}.
 Arguments state_upd_used_proph_id _ !_ /.
 
+Fixpoint heap_array (l : loc) (vs : list val) : gmap loc val :=
+  match vs with
+  | [] => ∅
+  | v :: vs' => {[l := v]} ∪ heap_array (l +ₗ 1) vs'
+  end.
+
+Lemma heap_array_singleton l v : heap_array l [v] = {[l := v]}.
+Proof. by rewrite /heap_array right_id. Qed.
+
+Lemma heap_array_lookup l vs w k :
+  heap_array l vs !! k = Some w ↔
+  ∃ j, 0 ≤ j ∧ k = l +ₗ j ∧ vs !! (Z.to_nat j) = Some w.
+Proof.
+  revert k l; induction vs as [|v' vs IH]=> l' l /=.
+  { rewrite lookup_empty. naive_solver lia. }
+  rewrite -insert_union_singleton_l lookup_insert_Some IH. split.
+  - intros [[-> ->] | (Hl & j & ? & -> & ?)].
+    { exists 0. rewrite loc_add_0. naive_solver lia. }
+    exists (1 + j). rewrite loc_add_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia.
+  - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
+    { rewrite loc_add_0; eauto. }
+    right. split.
+    { rewrite -{1}(loc_add_0 l). intros ?%(inj _); lia. }
+    assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
+    { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
+    rewrite Hj /= in Hil.
+    exists (j - 1). rewrite loc_add_assoc Z.add_sub_assoc Z.add_simpl_l.
+    auto with lia.
+Qed.
+
+Lemma heap_array_map_disjoint (h : gmap loc val) (l : loc) (vs : list val) :
+  (∀ i, (0 ≤ i) → (i < length vs) → h !! (l +ₗ i) = None) →
+  (heap_array l vs) ##ₘ h.
+Proof.
+  intros Hdisj. apply map_disjoint_spec=> l' v1 v2.
+  intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup.
+  move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj.
+Qed.
+
+Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
+  state_upd_heap (λ h, h ∪ heap_array l (replicate (Z.to_nat n) v)) σ.
+
 Inductive head_step : expr → state → list observation → expr → state → list expr → Prop :=
   | RecS f x e σ :
      head_step (Rec f x e) σ [] (Val $ RecV f x e) σ []
@@ -497,11 +547,12 @@ Inductive head_step : expr → state → list observation → expr → state →
      head_step (Case (Val $ InjRV v) e1 e2) σ [] (App e2 (Val v)) σ []
   | ForkS e σ:
      head_step (Fork e) σ [] (Val $ LitV LitUnit) σ [e]
-  | AllocS v σ l :
-     σ.(heap) !! l = None →
-     head_step (Alloc $ Val v) σ
+  | AllocNS n v σ l :
+     0 < n →
+     (∀ i, 0 ≤ i → i < n → σ.(heap) !! (l +ₗ i) = None) →
+     head_step (AllocN (Val $ LitV $ LitInt n) (Val v)) σ
                []
-               (Val $ LitV $ LitLoc l) (state_upd_heap <[l:=v]> σ)
+               (Val $ LitV $ LitLoc l) (state_init_heap l n v σ)
                []
   | LoadS l v σ :
      σ.(heap) !! l = Some v →
@@ -561,10 +612,17 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
   fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
 Proof. destruct Ki1, Ki2; intros; by simplify_eq. Qed.
 
-Lemma alloc_fresh v σ :
-  let l := fresh (dom (gset loc) σ.(heap)) in
-  head_step (Alloc $ Val v) σ [] (Val $ LitV $ LitLoc l) (state_upd_heap <[l:=v]> σ) [].
-Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
+Lemma alloc_fresh v n σ :
+  let l := fresh_locs (dom (gset loc) σ.(heap)) n in
+  0 < n →
+  head_step (AllocN ((Val $ LitV $ LitInt $ n)) (Val v)) σ []
+            (Val $ LitV $ LitLoc l) (state_init_heap l n v σ) [].
+Proof.
+  intros.
+  apply AllocNS; first done.
+  intros. apply (not_elem_of_dom (D := gset loc)).
+  by apply fresh_locs_fresh.
+Qed.
 
 Lemma new_proph_id_fresh σ :
   let p := fresh σ.(used_proph_id) in
@@ -594,6 +652,7 @@ Notation LamV x e := (RecV BAnon x e) (only parsing).
 Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing).
 Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing).
+Notation Alloc e := (AllocN (Val $ LitV $ LitInt 1) e) (only parsing).
 
 (* Skip should be atomic, we sometimes open invariants around
    it. Hence, we need to explicitly use LamV instead of e.g., Seq. *)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 8974f96faeb0f98840bfde988202f963956d1da9..514c533d8e3ed8451e15bfa47b2d231f7aea2097 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -53,7 +53,7 @@ Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core
 Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
 Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
 Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
-Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh : core.
+Local Hint Extern 0 (head_step (AllocN _ _) _ _ _ _ _) => apply alloc_fresh : core.
 Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
 Local Hint Resolve to_of_val : core.
 
@@ -67,7 +67,7 @@ Local Ltac solve_atomic :=
     [inversion 1; naive_solver
     |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].
 
-Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
+Instance alloc_atomic s v w : Atomic s (AllocN (Val v) (Val w)).
 Proof. solve_atomic. Qed.
 Instance load_atomic s v : Atomic s (Load (Val v)).
 Proof. solve_atomic. Qed.
@@ -184,24 +184,101 @@ Proof.
   iIntros (κ v2 σ2 efs Hstep); inv_head_step. by iFrame.
 Qed.
 
+Definition array (l : loc) (vs : list val) : iProp Σ :=
+  ([∗ list] i ↦ v ∈ vs, loc_add l i ↦ v)%I.
+
+Notation "l ↦∗ vs" := (array l vs)
+  (at level 20, format "l  ↦∗  vs") : bi_scope.
+
+Lemma array_nil l : l ↦∗ [] ⊣⊢ emp.
+Proof. by rewrite /array. Qed.
+
+Lemma array_singleton l v : l ↦∗ [v] ⊣⊢ l ↦ v.
+Proof. by rewrite /array /= right_id loc_add_0. Qed.
+
+Lemma array_app l vs ws :
+  l ↦∗ (vs ++ ws) ⊣⊢ l ↦∗ vs ∗ (loc_add l (length vs)) ↦∗ ws.
+Proof.
+  rewrite /array big_sepL_app.
+  setoid_rewrite Nat2Z.inj_add.
+  by setoid_rewrite loc_add_assoc.
+Qed.
+
+Lemma array_cons l v vs : l ↦∗ (v :: vs) ⊣⊢ l ↦ v ∗ (l +ₗ 1) ↦∗ vs.
+Proof.
+  rewrite /array big_sepL_cons loc_add_0.
+  setoid_rewrite loc_add_assoc.
+  setoid_rewrite Nat2Z.inj_succ.
+  by setoid_rewrite Z.add_1_l.
+Qed.
+
+Lemma heap_array_to_array l vs :
+  ([∗ map] i ↦ v ∈ heap_array l vs, i ↦ v)%I -∗ l ↦∗ vs.
+Proof.
+  iIntros "Hvs".
+  iInduction vs as [|v vs] "IH" forall (l); simpl.
+  { by rewrite big_opM_empty /array big_opL_nil. }
+  rewrite big_opM_union; last first.
+  { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
+    intros (j&?&Hjl&_)%heap_array_lookup.
+    rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl;
+      apply loc_add_inj in Hjl; lia. }
+  rewrite array_cons.
+  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]".
+  by iApply "IH".
+Qed.
+
 (** Heap *)
+Lemma wp_allocN s E v n :
+  0 < n →
+  {{{ True }}} AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
+  {{{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }}}.
+Proof.
+  iIntros (Hn Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κ κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
+  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  { symmetry.
+    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+    rewrite replicate_length Z2Nat.id; auto with lia. }
+  iModIntro; iSplit; auto.
+  iFrame. iApply "HΦ".
+  by iApply heap_array_to_array.
+Qed.
+Lemma twp_allocN s E v n :
+  0 < n →
+  [[{ True }]] AllocN ((Val $ LitV $ LitInt $ n)) (Val v) @ s; E
+  [[{ l, RET LitV (LitLoc l); l ↦∗ (replicate (Z.to_nat n) v) }]].
+Proof.
+  iIntros (Hn Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1 κs k) "[Hσ Hκs] !>"; iSplit; first by destruct n; auto with lia.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_alloc_gen with "Hσ") as "[Hσ Hl]".
+  { symmetry.
+    apply (heap_array_map_disjoint _ l (replicate (Z.to_nat n) v)); eauto.
+    rewrite replicate_length Z2Nat.id; auto with lia. }
+  iModIntro; iSplit; auto.
+  iFrame; iSplit; auto. iApply "HΦ".
+  by iApply heap_array_to_array.
+Qed.
+
 Lemma wp_alloc s E v :
   {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
-  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κ κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
-  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+  iIntros (Φ) "_ HΦ".
+  iApply wp_allocN; auto with lia.
+  iNext; iIntros (l) "H".
+  iApply "HΦ".
+  by rewrite array_singleton.
 Qed.
 Lemma twp_alloc s E v :
   [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
-  iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1 κs n) "[Hσ Hκs] !>"; iSplit; first by auto.
-  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
-  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
-  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
+  iIntros (Φ) "_ HΦ".
+  iApply twp_allocN; auto with lia.
+  iIntros (l) "H".
+  iApply "HΦ".
+  by rewrite array_singleton.
 Qed.
 
 Lemma wp_load s E l q v :
@@ -336,3 +413,6 @@ Proof.
 Qed.
 
 End lifting.
+
+Notation "l ↦∗ vs" := (array l vs)
+  (at level 20, format "l  ↦∗  vs") : bi_scope.
diff --git a/theories/heap_lang/locations.v b/theories/heap_lang/locations.v
new file mode 100644
index 0000000000000000000000000000000000000000..e10269515827f31b0c919b3b9a5a07d91b0eecff
--- /dev/null
+++ b/theories/heap_lang/locations.v
@@ -0,0 +1,44 @@
+From iris.algebra Require Import base.
+From stdpp Require Import countable numbers gmap.
+
+Record loc := { loc_car : Z }.
+
+Instance loc_eq_decision : EqDecision loc.
+Proof. solve_decision. Qed.
+
+Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
+
+Instance loc_countable : Countable loc.
+Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
+
+Definition loc_add (l : loc) (off : Z) : loc :=
+  {| loc_car := loc_car l + off|}.
+
+Notation "l +â‚— off" := (loc_add l off) (at level 50, left associativity).
+
+Lemma loc_add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
+Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
+
+Lemma loc_add_0 l : l +â‚— 0 = l.
+Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
+
+Instance loc_add_inj l : Inj eq eq (loc_add l).
+Proof. destruct l; rewrite /Inj /loc_add /=; intros; simplify_eq; lia. Qed.
+
+Definition fresh_locs (g : gset loc) (n : Z) : loc :=
+  {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r)%Z 1%Z g |}.
+
+Lemma fresh_locs_fresh g n i :
+  (0 ≤ i)%Z → (i < n)%Z → (fresh_locs g n) +ₗ i ∉ g.
+Proof.
+  rewrite /fresh_locs /loc_add /=; intros Hil _ Hf; clear n.
+  cut (∀ x, x ∈ g →
+            loc_car x < set_fold (λ k r, ((1 + loc_car k) `max` r)%Z) 1%Z g)%Z.
+  { intros Hlem; apply Hlem in Hf; simpl in *; lia. }
+  clear Hf.
+  eapply (set_fold_ind_L
+            (λ z g, ∀ x : loc, x ∈ g → (loc_car x < z)%Z));
+    try set_solver by eauto with lia.
+Qed.
+
+Global Opaque fresh_locs.
diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index f5661364a60e81da213d435d5172d2ce12797397..523d29c7593f8e1259e194d5b321f3c40b3dcfab 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -10,9 +10,9 @@ 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 | Alloc e | Load e =>
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Load e =>
      is_closed_expr X e
-  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | AllocN e1 e2 | Store e1 e2 | FAA e1 e2
   | ResolveProph e1 e2 =>
      is_closed_expr X e1 && is_closed_expr X e2
   | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
@@ -85,6 +85,41 @@ Lemma subst_rec_ne' f y e x v :
   subst' x v (Rec f y e) = Rec f y (subst' x v e).
 Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
 
+Lemma  bin_op_eval_closed op v1 v2 v':
+  is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
+  is_closed_val v'.
+Proof.
+  rewrite /bin_op_eval /bin_op_eval_bool /bin_op_eval_int;
+    repeat case_match; by naive_solver.
+Qed.
+
+Lemma heap_closed_alloc σ l n w :
+  0 < n →
+  is_closed_val w →
+  map_Forall (λ _ v, is_closed_val v) (heap σ) →
+  (∀ i : Z, 0 ≤ i → i < n → heap σ !! (l +ₗ i) = None) →
+  map_Forall (λ _ v, is_closed_val v)
+             (heap σ ∪ heap_array l (replicate (Z.to_nat n) w)).
+Proof.
+  intros Hn Hw Hσ Hl.
+  eapply (map_Forall_ind
+            (λ k v, ((heap σ ∪ heap_array l (replicate (Z.to_nat n) w))
+                       !! k = Some v))).
+  - apply map_Forall_empty.
+  - intros m i x Hi Hix Hkwm Hm.
+    apply map_Forall_insert_2; auto.
+    apply lookup_union_Some in Hix; last first.
+    { symmetry; eapply heap_array_map_disjoint;
+        rewrite replicate_length Z2Nat.id; auto with lia. }
+    destruct Hix as [[j Hj]%elem_of_map_to_list%elem_of_list_lookup_1|
+                     (?&?&?&[-> Hlt%inj_lt]%lookup_replicate_1)%heap_array_lookup].
+    { apply map_Forall_to_list in Hσ.
+      by eapply Forall_lookup in Hσ; eauto; simpl in *. }
+    rewrite !Z2Nat.id in Hlt; eauto with lia.
+  - apply map_Forall_to_list, Forall_forall.
+    intros [? ?]; apply elem_of_map_to_list.
+Qed.
+
 (* The stepping relation preserves closedness *)
 Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
   is_closed_expr [] e1 →
@@ -99,7 +134,8 @@ Proof.
     try apply map_Forall_insert_2; try by naive_solver.
   - subst. repeat apply is_closed_subst'; naive_solver.
   - unfold un_op_eval in *. repeat case_match; naive_solver.
-  - unfold bin_op_eval, bin_op_eval_bool in *. repeat case_match; naive_solver.
+  - eapply bin_op_eval_closed; eauto; naive_solver.
+  - by apply heap_closed_alloc.
 Qed.
 
 (* Parallel substitution with maps of values indexed by strings *)
@@ -131,7 +167,7 @@ Fixpoint subst_map (vs : gmap string val) (e : expr) : expr :=
   | InjR e => InjR (subst_map vs e)
   | Case e0 e1 e2 => Case (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
   | Fork e => Fork (subst_map vs e)
-  | Alloc e => Alloc (subst_map vs e)
+  | AllocN e1 e2 => AllocN (subst_map vs e1) (subst_map vs e2)
   | Load e => Load (subst_map vs e)
   | Store e1 e2 => Store (subst_map vs e1) (subst_map vs e2)
   | CAS e0 e1 e2 => CAS (subst_map vs e0) (subst_map vs e1) (subst_map vs e2)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 8519e3ec99abaffba8b9e81cf65b41cf8c3475ef..27db5d2c7f08ce51c7ed863c99e527e0b2f92406 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -177,6 +177,35 @@ Implicit Types Δ : envs (uPredI (iResUR Σ)).
 Implicit Types v : val.
 Implicit Types z : Z.
 
+Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
+  0 < n →
+  MaybeIntoLaterNEnvs 1 Δ Δ' →
+  (∀ l, ∃ Δ'',
+    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ' = Some Δ'' ∧
+    envs_entails Δ'' (WP fill K (Val $ LitV l) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (AllocN #n v) @ s; E {{ Φ }}).
+Proof.
+  rewrite envs_entails_eq=> ? ? HΔ.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
+  rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
+  by rewrite right_id HΔ'.
+Qed.
+Lemma tac_twp_allocN Δ s E j K v n Φ :
+  0 < n →
+  (∀ l, ∃ Δ',
+    envs_app false (Esnoc Enil j (array l (replicate (Z.to_nat n) v))) Δ
+    = Some Δ' ∧
+    envs_entails Δ' (WP fill K (Val $ LitV l) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (AllocN #n v) @ s; E [{ Φ }]).
+Proof.
+  rewrite envs_entails_eq=> ? HΔ.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
+  rewrite left_id. apply forall_intro=> l.
+  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
+  by rewrite right_id HΔ'.
+Qed.
+
 Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
   MaybeIntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
@@ -404,18 +433,43 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
         [pm_reflexivity || fail "wp_alloc:" H "not fresh"
         |iDestructHyp Htmp as H; wp_finish] in
   wp_pures;
+  (** The code first tries to use allocation lemma for a single reference,
+     ie, [tac_wp_alloc] (respectively, [tac_twp_alloc]).
+     If that fails, it tries to use the lemma [tac_wp_allocN]
+     (respectively, [tac_twp_allocN]) for allocating an array.
+     Notice that we could have used the array allocation lemma also for single
+     references. However, that would produce the resource l ↦∗ [v] instead of
+     l ↦ v for single references. These are logically equivalent assertions
+     but are not equal. *)
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-    first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
-      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    [iSolveTC
-    |finish ()]
+    let process_single _ :=
+        first
+          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc _ _ _ _ Htmp K))
+          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+        [iSolveTC
+        |finish ()]
+    in
+    let process_array _ :=
+        first
+          [reshape_expr e ltac:(fun K e' => eapply (tac_wp_allocN _ _ _ _ Htmp K))
+          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+        [idtac|iSolveTC
+         |finish ()]
+    in (process_single ()) || (process_array ())
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
-    first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
-      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
-    finish ()
+    let process_single _ :=
+        first
+          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_alloc _ _ _ Htmp K))
+          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+        finish ()
+    in
+    let process_array _ :=
+        first
+          [reshape_expr e ltac:(fun K e' => eapply (tac_twp_allocN _ _ _ Htmp K))
+          |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+        finish ()
+    in (process_single ()) || (process_array ())
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 4d5bbff3f43e244beb1c4fcb21fb7b6091defdc4..400da8c119820eba3ae8e164abf2f55efb841a48 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -22,7 +22,8 @@ Ltac reshape_expr e tac :=
   | InjL ?e => go (InjLCtx :: K) e
   | InjR ?e => go (InjRCtx :: K) e
   | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
-  | Alloc ?e => go (AllocCtx :: K) e
+  | AllocN ?e (Val ?v) => go (AllocNLCtx v :: K) e
+  | AllocN ?e1 ?e2 => go (AllocNRCtx e1 :: K) e2
   | Load ?e => go (LoadCtx :: K) e
   | Store ?e (Val ?v) => go (StoreLCtx v :: K) e
   | Store ?e1 ?e2 => go (StoreRCtx e1 :: K) e2