diff --git a/_CoqProject b/_CoqProject
index 171922776790384c6c28f2cc85fc74aa7732ac83..62bf39eebb52fe94fcb8ce35984e7c18e73af8ba 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -48,3 +48,4 @@ theories/tests/typetest.v
 theories/tests/ghosttp.v
 theories/tests/tactics.v
 theories/tests/tactics2.v
+theories/examples/coqpl.v
diff --git a/theories/examples/coqpl.v b/theories/examples/coqpl.v
new file mode 100644
index 0000000000000000000000000000000000000000..1d35c81501c5a9ce2c67249186c03cdf8ad56d3d
--- /dev/null
+++ b/theories/examples/coqpl.v
@@ -0,0 +1,90 @@
+From iris.proofmode Require Import tactics.
+From iris_logrel Require Import logrel.
+
+Section refinement.
+  Context `{logrelG Σ}.
+
+  Notation D := (prodC valC valC -n> iProp Σ).
+  Program Definition valrel' : (val * val → iProp Σ) → D :=
+    fun f => λne x, f x.
+  Solve Obligations with solve_proper.
+  Definition valrel (f : val → val → iProp Σ) : D :=
+    valrel' $ λ vv, f (vv.1) (vv.2).
+
+  Lemma test_goal Δ Γ (l l' : loc) :
+    l ↦ᵢ #1 -∗ l' ↦ₛ #0 -∗
+    {Δ;Γ} ⊨ !#l ≤log≤ (#l' <- #1;; !#l') : TNat.
+  Proof.
+    iIntros "Hl Hl'".
+    rel_store_r. rel_pure_r _.
+    rel_load_l. rel_load_r.
+    iApply bin_log_related_nat.
+  Qed.
+
+  Definition bitτ : type := ∃: TVar 0 × (TVar 0 → TVar 0) × (TVar 0 → Bool).
+
+  Definition bit_bool : val :=
+    pack (#true, (λ: "b", "b" ⊕ #true), (λ: "b", "b")).
+
+  Definition flip_nat : val := λ: "n",
+    if: ("n" = #0) then #1 else #0.
+  Definition bit_nat : val :=
+    pack (#1, flip_nat, (λ: "b", "b" = #1)).
+  
+  Definition f (b : bool) : nat := if b then 1 else 0.
+  (* R ⊆ Bool × Nat = { (true, 1), (false, 0) }*)
+  Definition R : D := valrel $ λ v1 v2,
+    (∃ b : bool, ⌜v1 = #b⌝ ∗ ⌜v2 = #(f b)⌝)%I.
+
+  Instance R_persistent ww : Persistent (R ww).
+  Proof. apply _. Qed.
+
+  Lemma bit_prerefinement Δ Γ :
+    {Δ;Γ} ⊨ bit_bool ≤log≤ bit_nat : bitτ.
+  Proof.
+    unfold bit_bool, bit_nat, flip_nat; simpl. (* we need this to compute the coercion from values to expression *)
+    iApply (bin_log_related_pack _ R).
+    repeat iApply bin_log_related_pair.
+    - rel_finish.
+    - iApply bin_log_related_arrow_val; try by unlock. cbn-[R].
+      iIntros "!#" (v1 v2) "/=".
+      iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
+      rel_rec_l. rel_rec_r.
+      rel_op_l. rel_op_r.
+      destruct b; simpl; rel_if_r; rel_finish.
+    - iApply bin_log_related_arrow_val; try by unlock.
+      iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *)
+      iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
+      rel_rec_l. rel_rec_r.
+      rel_op_r.
+      destruct b; rel_finish.
+  Qed.
+
+  Definition N : namespace := nroot.@"PL".@"Coq".
+
+  Lemma higher_order_stateful Δ Γ :
+    {Δ;Γ} ⊨
+      let: "x" := ref #1 in
+      (λ: "f", "f" #();; !"x")
+    ≤log≤
+      (λ: "f", "f" #();; #1)
+    : ((Unit → Unit) → TNat).
+  Proof.
+    rel_alloc_l as l "Hl".
+    rel_let_l.
+    iMod (inv_alloc N _ (l ↦ᵢ #1)%I with "Hl") as "#Hinv".
+    iApply bin_log_related_arrow; auto.
+    iIntros "!#" (f1 f2) "#Hf".
+    rel_let_l; rel_let_r.
+    iApply (bin_log_related_seq with "[Hf]"); auto.
+    - iApply (bin_log_related_app with "Hf").
+      iApply bin_log_related_unit.
+    - rel_load_l_atomic;
+      iInv N as "Hl" "Hcl"; iModIntro.
+      iExists #1. iNext. iFrame "Hl". simpl.
+      iIntros "Hl".
+      iMod ("Hcl" with "Hl") as "_".
+      iApply bin_log_related_nat.
+  Qed.
+  
+End refinement.