diff --git a/_CoqProject b/_CoqProject
index 3c324c7a1e1c4ef89151943fff4d995902ac2f27..ea94fda20d1a51a15b08fdf85b09ed0d1ed6c1ef 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,3 +8,4 @@ theories/channel/proto_model.v
 theories/channel/proto_channel.v
 theories/examples/list_sort.v
 theories/examples/list_sort_instances.v
+theories/examples/loop_sort.v
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index dfb91f0e0d1152b29cb9d0fb5a37a54adc37c312..825924714786ae06f12db190054969c4605ca774 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -36,17 +36,6 @@ Definition list_sort_service : val :=
     "xs" <- lmerge "cmp" !"ys" !"zs";;
     send "c" #().
 
-Definition loop_sort_service_go : val :=
-  rec: "go" "c" :=
-    if: recv "c" then list_sort_service "c";; "go" "c"
-    else if: recv "c" then
-      let: "d" := start_chan "go" in
-      send "c" "d";;
-      "go" "c"
-    else #().
-Definition loop_sort_service : val := λ: <>,
-  start_chan loop_sort_service_go.
-
 Definition list_sort_client : val := λ: "cmp" "xs",
   let: "c" := start_chan list_sort_service in
   send "c" "cmp";; send "c" "xs";;
@@ -155,38 +144,6 @@ Section list_sort.
     - rewrite (merge_Permutation R). by f_equiv.
   Qed.
 
-  Definition loop_sort_protocol_aux (rec : iProto Σ) : iProto Σ :=
-    ((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.
-
-  Instance loop_sort_protocol_aux_contractive : Contractive loop_sort_protocol_aux.
-  Proof.
-    intros n p p' Hp. rewrite /loop_sort_protocol_aux.
-    f_contractive; f_equiv=> //. apply iProto_message_ne=> c /=; by repeat f_equiv.
-  Qed.
-  Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
-  Lemma loop_sort_protocol_unfold :
-    loop_sort_protocol ≡ loop_sort_protocol_aux loop_sort_protocol.
-  Proof. apply (fixpoint_unfold loop_sort_protocol_aux). Qed.
-
-  Lemma loop_sort_service_go_spec c :
-    {{{ c ↣ iProto_dual loop_sort_protocol @ N }}}
-      loop_sort_service_go c
-    {{{ RET #(); c ↣ END @ N }}}.
-  Proof.
-    iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
-    wp_rec. rewrite {2}loop_sort_protocol_unfold.
-    wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
-    { wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
-      by wp_apply ("IH" with "Hc"). }
-    wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
-    - wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
-      { wp_apply ("IH" with "Hd"); auto. }
-      wp_apply (send_proto_spec with "Hc"); simpl.
-      iExists d; iSplit; first done. iIntros "{$Hd} !> Hc".
-      by wp_apply ("IH" with "Hc").
-    - by iApply "HΨ".
-  Qed.
-
   Lemma list_sort_client_spec {A} (I : A → val → iProp Σ) R
        `{!RelDecision R, !Total R} cmp l (vs : list val) (xs : list A) :
     cmp_spec I R cmp -∗
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
new file mode 100644
index 0000000000000000000000000000000000000000..8bdfe71951b432ddddf0a7e3ea6c4d8238b806a2
--- /dev/null
+++ b/theories/examples/loop_sort.v
@@ -0,0 +1,52 @@
+From stdpp Require Import sorting.
+From osiris.channel Require Import proto_channel.
+From iris.heap_lang Require Import proofmode notation.
+From osiris.utils Require Import list.
+From osiris.examples Require Import list_sort.
+
+Definition loop_sort_service : val :=
+  rec: "go" "c" :=
+    if: recv "c" then list_sort_service "c";; "go" "c"
+    else if: recv "c" then
+      let: "d" := start_chan "go" in
+      send "c" "d";;
+      "go" "c"
+    else #().
+
+Section loop_sort.
+  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
+
+  
+  Definition loop_sort_protocol_aux (rec : iProto Σ) : iProto Σ :=
+    ((sort_protocol <++> rec) <+> ((<?> c, MSG c {{ c ↣ rec @ N }}; rec) <+> END))%proto.
+
+  Instance loop_sort_protocol_aux_contractive : Contractive loop_sort_protocol_aux.
+  Proof.
+    intros n p p' Hp. rewrite /loop_sort_protocol_aux.
+    f_contractive; f_equiv=> //. apply iProto_message_ne=> c /=; by repeat f_equiv.
+  Qed.
+  Definition loop_sort_protocol : iProto Σ := fixpoint loop_sort_protocol_aux.
+  Lemma loop_sort_protocol_unfold :
+    loop_sort_protocol ≡ loop_sort_protocol_aux loop_sort_protocol.
+  Proof. apply (fixpoint_unfold loop_sort_protocol_aux). Qed.
+
+  Lemma loop_sort_service_spec c :
+    {{{ c ↣ iProto_dual loop_sort_protocol @ N }}}
+      loop_sort_service c
+    {{{ RET #(); c ↣ END @ N }}}.
+  Proof.
+    iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
+    wp_rec. rewrite {2}loop_sort_protocol_unfold.
+    wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
+    { wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
+      by wp_apply ("IH" with "Hc"). }
+    wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
+    - wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
+      { wp_apply ("IH" with "Hd"); auto. }
+      wp_apply (send_proto_spec with "Hc"); simpl.
+      iExists d; iSplit; first done. iIntros "{$Hd} !> Hc".
+      by wp_apply ("IH" with "Hc").
+    - by iApply "HΨ".
+  Qed.
+
+End loop_sort.
\ No newline at end of file