diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b37214d146d6153e98ec3794ee6f988751b01a2..d8d228dc633630c261d424f221d7719d3ee6db05 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -93,6 +93,7 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Some extensions/improvements of heap_lang:
   - Improve handling of pure (non-state-dependent) reductions.
   - Add fetch-and-add (`FAA`) operation.
+  - Syntax for all Coq's binary operations on `Z`.
 * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index f9eee0ab9710207e73b2c6e288d256f391d4060d..45f540eceb521c8268ac27054fa2720bbb402d86 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -15,7 +15,10 @@ Inductive base_lit : Set :=
 Inductive un_op : Set :=
   | NegOp | MinusUnOp.
 Inductive bin_op : Set :=
-  | PlusOp | MinusOp | LeOp | LtOp | EqOp.
+  | PlusOp | MinusOp | MultOp | QuotOp | RemOp (* Arithmetic *)
+  | AndOp | OrOp | XorOp (* Bitwise *)
+  | ShiftLOp | ShiftROp (* Shifts *)
+  | LeOp | LtOp | EqOp. (* Relations *)
 
 Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope binder_scope with bind.
@@ -158,9 +161,13 @@ Qed.
 Instance bin_op_countable : Countable bin_op.
 Proof.
  refine (inj_countable' (λ op, match op with
-  | PlusOp => 0 | MinusOp => 1 | LeOp => 2 | LtOp => 3 | EqOp => 4
+  | 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
   end) (λ n, match n with
-  | 0 => PlusOp | 1 => MinusOp | 2 => LeOp | 3 => LtOp | _ => EqOp
+  | 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
   end) _); by intros [].
 Qed.
 Instance binder_countable : Countable binder.
@@ -310,18 +317,44 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
 Definition un_op_eval (op : un_op) (v : val) : option val :=
   match op, v with
   | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
+  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
   | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
   | _, _ => None
   end.
 
+Definition bin_op_eval_int (op : bin_op) (n1 n2 : Z) : 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))
+  end.
+
+Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
+  match op with
+  | PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
+  | AndOp => Some (LitBool (b1 && b2))
+  | OrOp => Some (LitBool (b1 || b2))
+  | XorOp => Some (LitBool (xorb b1 b2))
+  | ShiftLOp | ShiftROp => None (* Shifts *)
+  | LeOp | LtOp => None (* InEquality *)
+  | EqOp => Some (LitBool (bool_decide (b1 = b2)))
+  end.
+
 Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
-  match op, v1, v2 with
-  | PlusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 + n2)
-  | MinusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 - n2)
-  | LeOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 ≤ n2)
-  | LtOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 < n2)
-  | EqOp, v1, v2 => Some $ LitV $ LitBool $ bool_decide (v1 = v2)
-  | _, _, _ => None
+  match v1, v2 with
+  | LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ bin_op_eval_int op n1 n2
+  | LitV (LitBool b1), LitV (LitBool b2) => LitV <$> bin_op_eval_bool op b1 b2
+  | v1, v2 => guard (op = EqOp); Some $ LitV $ LitBool $ bool_decide (v1 = v2)
   end.
 
 Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index 0ee932730a1f67c4a9f79476bbc30b352938d615..3751417fa10d2a6f30996a34389d880a86993bcb 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -58,16 +58,21 @@ Notation "()" := LitUnit : val_scope.
 Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
 Notation "'ref' e" := (Alloc e%E)
   (at level 30, right associativity) : expr_scope.
-Notation "- e" := (UnOp MinusUnOp e%E)
-  (at level 35, right associativity) : expr_scope.
-Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
-  (at level 50, left associativity) : expr_scope.
-Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
-  (at level 50, left associativity) : expr_scope.
-Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope.
-Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope.
-Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
-Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr_scope.
+Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.
+
+Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
+Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
+Notation "e1 `quot` e2" := (BinOp QuotOp e1%E e2%E) : expr_scope.
+Notation "e1 `rem` e2" := (BinOp RemOp e1%E e2%E) : expr_scope.
+Notation "e1 ≪ e2" := (BinOp ShiftLOp e1%E e2%E) : expr_scope.
+Notation "e1 ≫ e2" := (BinOp ShiftROp e1%E e2%E) : expr_scope.
+
+Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope.
+Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
+Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) : expr_scope.
+
 Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.