diff --git a/CHANGELOG.md b/CHANGELOG.md
index 54539dc6abce61ebea1a21f96d7eeb1f40a04174..82dab0b08df33e50c9d21c389dce01813adf01b6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -78,6 +78,7 @@ Coq 8.13 is no longer supported.
 * Move operations and lemmas about locations into a module `Loc`.
 * Extend `wp_apply` and `wp_smart_apply` to support immediately introducing the
   postcondition into the context via `as (x1 ... xn) "ipat1 ... ipatn"`.
+* Add comparison `≤` and `<` for locations. (by Arthur Azevedo de Amorim).
 
 **LaTeX changes:**
 
diff --git a/iris_heap_lang/lang.v b/iris_heap_lang/lang.v
index f75cdc21161ff46c8cab2778a811a0efdef641df..046a7beb31fb6e0f325ee0a518e0486f0564fb12 100644
--- a/iris_heap_lang/lang.v
+++ b/iris_heap_lang/lang.v
@@ -560,6 +560,8 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
   match op, v2 with
   | OffsetOp, LitInt off => Some $ LitLoc (l1 +â‚— off)
+  | LeOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 ≤ₗ l2))
+  | LtOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 <â‚— l2))
   | _, _ => None
   end.
 
diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 631e1be25d7a105c69312bd19b2401bc10c2b93a..92c562bb7da3d91ad74d78a8da6ca93722aa4a7e 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -27,9 +27,15 @@ Module Loc.
   Definition add (l : loc) (off : Z) : loc :=
     {| loc_car := loc_car l + off|}.
 
+  Definition le (l1 l2 : loc) : Prop := loc_car l1 ≤ loc_car l2.
+
+  Definition lt (l1 l2 : loc) : Prop := loc_car l1 < loc_car l2.
+
   Module Import notations.
     Notation "l +â‚— off" :=
       (add l off) (at level 50, left associativity) : stdpp_scope.
+    Notation "l1 ≤ₗ l2" := (le l1 l2) (at level 70) : stdpp_scope.
+    Notation "l1 <â‚— l2" := (lt l1 l2) (at level 70) : stdpp_scope.
   End notations.
 
   Lemma add_assoc l i j : l +â‚— i +â‚— j = l +â‚— (i + j).
@@ -41,6 +47,33 @@ Module Loc.
   Global Instance add_inj l : Inj eq eq (add l).
   Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.
 
+  Global Instance le_dec l1 l2 : Decision (l1 ≤ₗ l2).
+  Proof. rewrite /le. apply _. Qed.
+
+  Global Instance lt_dec l1 l2 : Decision (l1 <â‚— l2).
+  Proof. rewrite /lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder le.
+  Proof.
+    rewrite /le. split; [split|].
+    - by intros ?.
+    - intros [x] [y] [z]; lia.
+    - intros [x] [y] ??; f_equal/=; lia.
+  Qed.
+
+  Global Instance le_total : Total le.
+  Proof. rewrite /Total /le. lia. Qed.
+
+  Lemma le_ngt l1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
+  Proof. apply Z.le_ngt. Qed.
+
+  Lemma le_lteq l1 l2 : l1 ≤ₗ l2 ↔ l1 <ₗ l2 ∨ l1 = l2.
+  Proof. rewrite eq_spec. apply Z.le_lteq. Qed.
+
+  Lemma add_le_mono l1 l2 i1 i2 :
+    l1 ≤ₗ l2 → i1 ≤ i2 → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
+  Proof. apply Z.add_le_mono. Qed.
+
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
 
diff --git a/iris_unstable/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
index 8d0771a77d52272a9683ff3a413b3e1ab0373abd..ed8ce71d1ce9035f94fd56233cb93252bd326b76 100644
--- a/iris_unstable/heap_lang/interpreter.v
+++ b/iris_unstable/heap_lang/interpreter.v
@@ -403,8 +403,12 @@ Section interpreter.
            match op, v2 with
            | OffsetOp, LitV (LitInt _) => None
            | OffsetOp, _ => Some $ "can only call +â‚— on integers, got " + v2
-           | _, _ => Some $ "the only supported operation on locations is +â‚— #i, got "
-                            + op + " " + v2
+           | LeOp, LitV (LitLoc _) => None
+           | LeOp, _ => Some $ "cannot use ≤ on location " + v1 + " and " + v2
+           | LtOp, LitV (LitLoc _) => None
+           | LtOp, _ => Some $ "cannot use < on location " + v1 + " and " + v2
+           | _, _ => Some $ "the only supported operations on locations are " +
+                            " +ₗ #i, ≤ #l and < #l; got " + op + " " + v2
            end
          | _, _ => Some $ "mismatched types of values " + v1 + " and " + v2
          end.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 149c0c4ca507705593e020802c2d5f4f2719408c..7f3f6270b15aa9e56386f2deb505146664019bf2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -143,6 +143,22 @@ Section tests.
     by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
+  Definition compare_pointers : val := λ: <>,
+    let: "x" := ref #0 in
+    let: "y" := ref #0 in
+    ("x", "y", "x" ≤ "y").
+
+  Lemma wp_compare_pointers E :
+    ⊢ WP compare_pointers #() @ E [{ v, ∃ l1 l2 : loc,
+        ⌜v = (#l1, #l2,
+              #(bool_decide (loc_car l1 ≤ loc_car l2)))%V⌝ }].
+  Proof.
+    rewrite /compare_pointers. wp_pures.
+    wp_alloc l1 as "H1".
+    wp_alloc l2 as "H2".
+    wp_pures. by eauto.
+  Qed.
+
   (* Make sure [wp_bind] works even when it changes nothing. *)
   Lemma wp_bind_nop (e : expr) :
     ⊢ WP e + #0 {{ _, True }}.
diff --git a/tests/heap_lang_interpreter.ref b/tests/heap_lang_interpreter.ref
index e64c785499ae4b27529797347a7c43bfa93cf103..f64be950d43080de777bfef90de6512b8b59988a 100644
--- a/tests/heap_lang_interpreter.ref
+++ b/tests/heap_lang_interpreter.ref
@@ -24,9 +24,7 @@
      : val + Error
 "fail loc order"
      : string
-     = inr
-         (Stuck
-            "bin-op failed: the only supported operation on locations is +â‚— #i, got < #(loc 2)")
+     = inr (Stuck "bin-op failed: cannot use < on location #(loc 1) and #1")
      : val + Error
 "fail compare pairs"
      : string
diff --git a/tests/heap_lang_interpreter.v b/tests/heap_lang_interpreter.v
index bc91eac9d8b02f32889a1fb000d2aa185b9df981..5db79c1b5e557dc8562dfe0fca0bff75523617a0 100644
--- a/tests/heap_lang_interpreter.v
+++ b/tests/heap_lang_interpreter.v
@@ -47,11 +47,11 @@ Check "fail app non-function".
 Eval vm_compute in
     exec 1000 (#2 #4).
 
-(* locations are not ordered *)
+(* locations can only be compared with other locations *)
 Check "fail loc order".
 Eval vm_compute in
     exec 1000 (let: "x" := ref #() in
-               let: "y" := ref #() in
+               let: "y" := #1 in
                "x" < "y").
 
 Check "fail compare pairs".