diff --git a/_CoqProject b/_CoqProject
index 7a5a09844445ec9f8b1d0a1f8a59d0f5aef9bdbc..3a5b6444749e1172a08bce0e798c6d7dbade23f1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,3 +15,4 @@ theories/examples/proofs.v
 theories/examples/proofs_enc.v
 theories/examples/branching_examples.v
 theories/examples/branching_proofs.v
+theories/examples/list_sort.v
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index 1dc08c1e9c98e3438f261dc5349d41e5fa6cfa8c..5f9e8dd581580e04dca3c8e160df51926f665b05 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -70,7 +70,7 @@ Section channel.
   Context `{!heapG Σ, !chanG Σ} (N : namespace).
 
   Definition is_list_ref (l : val) (xs : list val) : iProp Σ :=
-    (∃ l':loc, ∃ hd : val, ⌜l = #l'⌝ ∧ l' ↦ hd ∗ ⌜is_list hd xs⌝)%I.
+    (∃ l':loc, ⌜l = #l'⌝ ∧ l' ↦ encode xs)%I.
 
   Record chan_name := Chan_name {
     chan_lock_name : gname;
@@ -119,8 +119,8 @@ Section channel.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
     wp_lam.
-    wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
-    wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
+    wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
+    wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
     iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
       as (lsγ) "[Hls Hls']"; first done.
     iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
@@ -164,8 +164,9 @@ Section channel.
     wp_apply get_side_spec; wp_pures.
     iDestruct (chan_inv_alt s with "Hinv") as
         (vs ws) "(Href & Hvs & Href' & Hws)".
-    iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
-    wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
+    iDestruct "Href" as (ll Hslr) "Hll". rewrite Hslr.
+    wp_load. 
+    wp_apply (lsnoc_spec (T:=val))=> //; iIntros (_).
     wp_bind (_ <- _)%E.
     iMod "HΦ" as (vs') "[Hchan HΦ]".
     iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
@@ -174,7 +175,7 @@ Section channel.
     iModIntro.
     wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
     iApply (chan_inv_alt s).
-    rewrite /is_list_ref. eauto 10 with iFrame.
+    rewrite /is_list_ref. eauto 20 with iFrame.
   Qed.
 
   Lemma try_recv_spec Φ E γ c s :
@@ -193,22 +194,20 @@ Section channel.
     wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
     iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
         (vs ws) "(Href & Hvs & Href' & Hws)".
-    iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
+    iDestruct "Href" as (ll Hslr) "Hll"; rewrite Hslr.
     wp_bind (! _)%E.
     iMod "HΦ" as (vs') "[Hchan HΦ]".
     wp_load.
     iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
     destruct vs as [|v vs]; simpl.
-    - iDestruct "Hlvs" as %->.
-      iDestruct "HΦ" as "[HΦ _]".
+    - iDestruct "HΦ" as "[HΦ _]".
       iMod ("HΦ" with "[//] Hchan") as "HΦ".
       iModIntro.
       wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
       { iApply (chan_inv_alt (dual_side s)).
         rewrite /is_list_ref. eauto 10 with iFrame. }
       iIntros (_). wp_pures. by iApply "HΦ".
-    - iDestruct "Hlvs" as %(hd' & -> & Hhd').
-      iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
+    - iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
       iDestruct "HΦ" as "[_ HΦ]".
       iMod ("HΦ" with "[//] Hchan") as "HΦ".
       iModIntro. wp_store.
diff --git a/theories/encodings/encodable.v b/theories/encodings/encodable.v
index 2f80f684b667d3f4e821f3717e4fab94f7c14aba..7fb375856187f1d9323a62ff9f2ad5452d7cf56b 100644
--- a/theories/encodings/encodable.v
+++ b/theories/encodings/encodable.v
@@ -64,3 +64,14 @@ Proof.
   - intros.
     apply decenc. eauto.
 Qed.
+
+Lemma enc_inj {A : Type} `{ED : EncDec A}
+      x y : encode x = encode y -> x = y.
+Proof.
+  intros Heq.
+  assert (decode (encode x) = decode (encode y)).
+  { by f_equiv. }
+  erewrite encdec in H=> //.
+  erewrite encdec in H=> //.
+  by inversion H.
+Qed.
\ No newline at end of file
diff --git a/theories/encodings/list.v b/theories/encodings/list.v
index 8039c93740ef94a44f516493dae19c53f0b89601..d1007df7162cd7ec5b896d27755401468859dfe8 100644
--- a/theories/encodings/list.v
+++ b/theories/encodings/list.v
@@ -1,11 +1,20 @@
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
+From osiris Require Export encodable.
 
 (** Immutable ML-style functional lists *)
-Fixpoint is_list (hd : val) (xs : list val) : Prop :=
+Instance pair_encodable `{Encodable A, Encodable B} : Encodable (A * B) :=
+  λ p, (encode p.1, encode p.2)%V.
+
+Instance option_encodable `{Encodable A} : Encodable (option A) := λ mx,
+  match mx with Some x => SOMEV (encode x) | None => NONEV end%V.
+
+Instance list_encodable `{Encodable A} : Encodable (list A) :=
+  fix go xs :=
+  let _ : Encodable _ := @go in
   match xs with
-  | [] => hd = NONEV
-  | x :: xs => ∃ hd', hd = SOMEV (x,hd') ∧ is_list hd' xs
+  | [] => encode None
+  | x :: xs => encode (Some (x,xs))
   end.
 
 Definition lnil : val := λ: <>, NONEV.
@@ -65,134 +74,110 @@ Definition lsnoc : val :=
 Section lists.
 Context `{heapG Σ}.
 Implicit Types i : nat.
-Implicit Types v : val.
+Context `{EncDec T}.
+Implicit Types x : T.
+Implicit Types xs : list T.
 
 Lemma lnil_spec :
-  {{{ True }}}
-    lnil #()
-  {{{ hd, RET hd; ⌜ is_list hd [] ⌝ }}}.
+  {{{ True }}} lnil #() {{{ RET encode []; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
 
-Lemma lcons_spec hd vs v :
-  {{{ ⌜ is_list hd vs ⌝ }}}
-    lcons v hd
-  {{{ hd', RET hd'; ⌜ is_list hd' (v :: vs) ⌝ }}}.
-Proof.
-  iIntros (Φ ?) "HΦ". wp_lam. wp_pures.
-  iApply "HΦ". simpl; eauto.
-Qed.
+Lemma lcons_spec x xs :
+  {{{ True }}} lcons (encode x) (encode xs) {{{ RET (encode (x :: xs)); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma lhead_spec x xs:
+  {{{ True }}} lhead (encode (x::xs)) {{{ RET encode x; True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
-Lemma lhead_spec hd vs v :
-  {{{ ⌜ is_list hd (v :: vs) ⌝ }}}
-    lhead hd
-  {{{ RET v; True }}}.
-Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-
-Lemma ltail_spec hd vs v :
-  {{{ ⌜ is_list hd (v :: vs) ⌝ }}}
-    ltail hd
-  {{{ hd', RET hd'; ⌜ is_list hd' vs ⌝ }}}.
-Proof. iIntros (Φ (hd'&->&?)) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-
-Lemma llookup_spec i hd vs v :
-  vs !! i = Some v →
-  {{{ ⌜ is_list hd vs ⌝ }}}
-    llookup #i hd
-  {{{ RET v; True }}}.
+Lemma ltail_spec x xs :
+  {{{ True }}} ltail (encode (x::xs)) {{{ RET encode xs; True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+Lemma llookup_spec i xs x:
+  xs !! i = Some x →
+  {{{ True }}}
+    llookup #i (encode xs)
+  {{{ RET encode x; True }}}.
 Proof.
   iIntros (Hi Φ Hl) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl);
+  iInduction xs as [|x' xs] "IH" forall (i Hi Hl);
     destruct i as [|i]=> //; simplify_eq/=.
   { wp_lam. wp_pures. by iApply (lhead_spec with "[//]"). }
   wp_lam. wp_pures.
-  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
+  wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
   wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
 Qed.
 
-Lemma linsert_spec i hd vs v :
-  is_Some (vs !! i) →
-  {{{ ⌜ is_list hd vs ⌝ }}}
-    linsert #i v hd
-  {{{ hd', RET hd'; ⌜ is_list hd' (<[i:=v]> vs) ⌝ }}}.
+Lemma linsert_spec i xs x :
+  is_Some (xs !! i) →
+  {{{ True }}}
+    linsert #i (encode x) (encode xs)
+  {{{ RET encode (<[i:=x]>xs); True }}}.
 Proof.
   iIntros ([w Hi] Φ Hl) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (hd i Hi Hl Φ);
+  iInduction xs as [|x' xs] "IH" forall (i Hi Hl Φ);
     destruct i as [|i]=> //; simplify_eq/=.
-  { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (hd' ?).
+  { wp_lam. wp_pures. wp_apply (ltail_spec with "[//]"). iIntros (?).
     wp_let. by iApply (lcons_spec with "[//]"). }
   wp_lam; wp_pures.
-  wp_apply (ltail_spec with "[//]"); iIntros (hd' ?). wp_let.
+  wp_apply (ltail_spec with "[//]"); iIntros (?). wp_let.
   wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
-  wp_apply ("IH" with "[//] [//]"). iIntros (hd'' ?). wp_let.
+  wp_apply ("IH" with "[//] [//]"). iIntros (?). wp_let.
   wp_apply (lhead_spec with "[//]"); iIntros "_".
   by wp_apply (lcons_spec with "[//]").
 Qed.
 
-Lemma llist_member_spec hd vs v :
-  {{{ ⌜ is_list hd vs ⌝ }}}
-    llist_member v hd
-  {{{ RET #(bool_decide (v ∈ vs)); True }}}.
+Lemma llist_member_spec `{EqDecision T} (xs : list T) (x : T) :
+  {{{ True }}}
+    llist_member (encode x) (encode xs)
+  {{{ RET #(bool_decide (x ∈ xs)); True }}}.
 Proof.
   iIntros (Φ Hl) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
+  iInduction xs as [|x' xs] "IH" forall (Hl); simplify_eq/=.
   { wp_lam; wp_pures. by iApply "HΦ". }
-  destruct Hl as (hd'&->&?). wp_lam; wp_pures.
-  destruct (bool_decide_reflect (v' = v)) as [->|?]; wp_if.
-  { rewrite (bool_decide_true (_ ∈ _ :: _)); last by left. by iApply "HΦ". }
+  wp_lam; wp_pures.
+  destruct (bool_decide_reflect (encode x' = encode x)) as [Heq|?]; wp_if.
+  { apply enc_inj in Heq. rewrite Heq. rewrite (bool_decide_true (_ ∈ _ :: _)). by iApply "HΦ". by left. }
   wp_proj. wp_let. iApply ("IH" with "[//]").
-  destruct (bool_decide_reflect (v ∈ vs)).
+  destruct (bool_decide_reflect (x ∈ xs)).
   - by rewrite bool_decide_true; last by right.
   - by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
 Qed.
 
-Lemma lreplicate_spec i v :
+Lemma lreplicate_spec i x :
   {{{ True }}}
-    lreplicate #i v
-  {{{ hd, RET hd; ⌜ is_list hd (replicate i v) ⌝ }}}.
+    lreplicate #i (encode x)
+  {{{ RET encode (replicate i x); True }}}.
 Proof.
   iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
   { wp_lam; wp_pures.
     iApply (lnil_spec with "[//]"). iApply "HΦ". }
   wp_lam; wp_pures.
   rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
-  wp_apply "IH"; iIntros (hd' Hl). wp_let. by iApply (lcons_spec with "[//]").
+  wp_apply "IH"; iIntros (Hl). wp_let. by iApply (lcons_spec with "[//]").
 Qed.
 
-Lemma llength_spec hd vs :
-  {{{ ⌜ is_list hd vs ⌝ }}} llength hd {{{ RET #(length vs); True }}}.
+Lemma llength_spec xs :
+  {{{ True }}} llength (encode xs) {{{ RET #(length xs); True }}}.
 Proof.
   iIntros (Φ Hl) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (hd Hl Φ); simplify_eq/=.
+  iInduction xs as [|x' xs] "IH" forall (Hl Φ); simplify_eq/=.
   { wp_lam. wp_match. by iApply "HΦ". }
-  destruct Hl as (hd'&->&?). wp_lam. wp_match. wp_proj.
-  wp_apply ("IH" $! hd' with "[//]"); iIntros "_ /=". wp_op.
+wp_lam. wp_match. wp_proj.
+  wp_apply ("IH" with "[//]"); iIntros "_ /=". wp_op.
   rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
 Qed.
 
-Lemma lsnoc_spec hd vs v :
-  {{{ ⌜ is_list hd vs ⌝ }}}
-    lsnoc hd v
-  {{{ hd', RET hd'; ⌜ is_list hd' (vs++[v]) ⌝ }}}.
+Lemma lsnoc_spec xs x :
+  {{{ True }}} lsnoc (encode xs) (encode x) {{{ RET (encode (xs++[x])); True }}}.
 Proof.
   iIntros (Φ Hvs) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (hd Hvs Φ).
-  - simplify_eq/=.
-    wp_rec.
-    wp_pures.
-    wp_lam.
-    wp_pures.
-    iApply "HΦ". simpl. eauto.
-  - destruct Hvs as [vs' [-> Hvs']].
-    wp_rec.
-    wp_pures.
-    wp_bind (lsnoc vs' v).
-    iApply "IH".
-    eauto.
-    iNext.
-    iIntros (hd' Hhd').
-    wp_pures.
-    iApply lcons_spec.
-    eauto.
-    iApply "HΦ".
+  iInduction xs as [|x' xs] "IH" forall (Hvs Φ).
+  { wp_rec. wp_pures. wp_lam. wp_pures. by iApply "HΦ". }
+  wp_rec.
+  wp_apply "IH"=> //.
+  iIntros (_). by wp_apply lcons_spec=> //.
 Qed.
+
 End lists.
\ No newline at end of file
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
new file mode 100644
index 0000000000000000000000000000000000000000..9706add78d30af6625e2dd5854d63031c1f1eaf0
--- /dev/null
+++ b/theories/examples/list_sort.v
@@ -0,0 +1,279 @@
+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Import proofmode notation.
+From osiris.typing Require Import side stype.
+From osiris.encodings Require Import list channel stype_enc.
+From iris.base_logic Require Import invariants.
+From stdpp Require Import sorting.
+Require Import Coq.Lists.List.
+Require Import Omega.
+
+Section ListSortExample.
+  Context `{!heapG Σ} `{logrelG val Σ} (N : namespace).
+
+  Definition lsplit : val :=
+    λ: "xs",
+      let: "hd" := lhead "xs" in
+      let: "ys" := lcons "hd" NONEV in
+      let: "zs" := ltail "xs" in
+    ("ys", "zs").
+
+  Lemma lsplit_spec (x : Z) (xs : list Z) :
+    {{{ True }}}
+      lsplit (encode (x::xs))
+    {{{ RET (encode [x],encode xs); True }}}.
+  Proof.
+    iIntros (Φ _) "HΦ".
+    wp_lam. wp_apply (lhead_spec (T := Z))=> //.
+    iIntros (_).
+    wp_apply (lcons_spec (T := Z) _ [])=> //.
+    iIntros (_).
+    wp_apply (ltail_spec (T := Z))=> //.
+    iIntros (_).
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+  Definition lsplit_ref : val :=
+    λ: "xs", let: "ys_zs" := lsplit !"xs" in
+             (ref (Fst "ys_zs"), ref (Snd ("ys_zs"))).
+
+  Lemma lsplit_ref_spec lxs (x : Z) (xs : list Z) :
+    {{{ lxs ↦ encode (x::xs) }}}
+      lsplit_ref #lxs
+    {{{ lys lzs ys zs, RET (#lys,#lzs);
+        ⌜(x::xs) = ys++zs⌝ ∗
+        lxs ↦ encode (x::xs) ∗
+        lys ↦ encode ys ∗
+        lzs ↦ encode zs }}}.
+  Proof.
+    iIntros (Φ) "Hhd HΦ".
+    wp_lam. wp_load. wp_apply (lsplit_spec)=> //; iIntros (_).
+    wp_alloc lzs as "Hlzs".
+    wp_alloc lys as "Hlys".
+    wp_pures.
+    iApply "HΦ".
+    eauto 10 with iFrame.
+  Qed.
+
+  Definition compare_vals : val :=
+    λ: "x" "y", "x" ≤ "y".
+
+  Lemma compare_vals_spec (x y : Z) :
+    {{{ True }}}
+      compare_vals (encode x) (encode y)
+    {{{ RET (encode (bool_decide (x ≤ y))); True }}}.
+  Proof. iIntros (Φ) "_ HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
+
+  Definition lmerge : val :=
+    rec: "go" "hys" "hzs" :=
+      if: llength "hys" = #0
+      then "hzs"
+      else if: llength "hzs" = #0
+           then "hys"
+           else let: "y" := lhead "hys" in
+                let: "z" := lhead "hzs" in
+                if: (compare_vals "y" "z")
+                then lcons "y" ("go" (ltail "hys") "hzs")
+                else lcons "z" ("go" "hys" (ltail "hzs")).
+
+  Lemma list_merge_emp1 (ys : list Z) : list_merge (≤) [] ys = ys.
+  Proof. induction ys; eauto. Qed.
+
+  Lemma list_merge_emp2 (xs : list Z) : list_merge (≤) xs [] = xs.
+  Proof. induction xs; eauto. Qed.
+
+  Lemma lmerge_spec (ys zs : list Z) :
+    {{{ True }}}
+      lmerge (encode ys) (encode zs)
+    {{{ RET (encode (list_merge (≤) ys zs)); True }}}.
+  Proof.
+    revert ys zs.
+    iLöb as "IH".
+    iIntros (ys zs Φ _) "HΦ".
+    wp_lam.
+    wp_apply (llength_spec (T:=Z))=> //; iIntros "_".
+    destruct ys as [|y ys].
+    { wp_pures. rewrite list_merge_emp1. by iApply ("HΦ"). }
+    wp_apply (llength_spec (T:=Z))=> //; iIntros "_".
+    destruct zs as [|z zs].
+    { wp_pures. by iApply ("HΦ"). }
+    wp_apply (lhead_spec (T:=Z))=> //; iIntros "_".
+    wp_apply (lhead_spec (T:=Z))=> //; iIntros "_".
+    wp_apply (compare_vals_spec)=> //; iIntros "_".
+    rewrite list_merge_cons.
+    destruct (decide (y ≤ z)).
+    - rewrite bool_decide_true=> //.
+      wp_apply (ltail_spec (T:=Z))=> //; iIntros (_).
+      wp_apply ("IH")=> //; iIntros (_).
+      wp_apply (lcons_spec (T:=Z))=> //.
+    - rewrite bool_decide_false=> //.
+      wp_apply (ltail_spec (T:=Z))=> //; iIntros (_).
+      wp_apply ("IH")=> //; iIntros (_).
+      wp_apply (lcons_spec (T:=Z))=> //.
+  Qed.
+
+  Definition lmerge_ref : val :=
+    λ: "lxs" "hys" "hzs",
+      "lxs" <- lmerge "hys" "hzs".
+
+  Lemma lmerge_ref_spec ldx tmp ys zs :
+    {{{ ldx ↦ tmp }}}
+      lmerge_ref #ldx (encode ys) (encode zs)
+    {{{ RET #(); ldx ↦ encode (list_merge (≤) ys zs) }}}.
+  Proof.
+    iIntros (Φ) "Hldx HΦ".
+    wp_lam.
+    wp_apply (lmerge_spec ys zs)=> //.
+    iIntros (_).
+    wp_store.
+    by iApply ("HΦ").
+  Qed.
+
+  Definition list_sort_service : val :=
+    rec: "go" "c" :=
+      let: "xs" := recv "c" #Right in
+      if: llength (!"xs") ≤ #1
+      then send "c" #Right "xs"
+      else let: "ys_zs" := lsplit_ref "xs" in
+           let: "ys" := Fst "ys_zs" in
+           let: "zs" := Snd "ys_zs" in
+           let: "cy" := new_chan #() in Fork("go" "cy");;
+           let: "cz" := new_chan #() in Fork("go" "cz");;
+           send "cy" #Left "ys";;
+           send "cz" #Left "zs";;
+           let: "ys" := recv "cy" #Left in
+           let: "zs" := recv "cz" #Left in
+           lmerge_ref "xs" !"ys" !"zs";;
+           send "c" #Right "xs".
+
+  Lemma list_sort_service_spec γ c xs :
+    {{{ ⟦ c @ Right : (<?> l @ l ↦ encode xs,
+                          <!> l' @
+                          ⌜l = l'⌝ ∗ (∃ ys : list Z,
+                                      l' ↦ encode ys ∗
+                                      ⌜Sorted (≤) ys⌝ ∗
+                                      ⌜Permutation ys xs⌝),
+                          TEnd) ⟧{N,γ} }}}
+      list_sort_service c
+    {{{ RET #(); ⟦ c @ Right : TEnd ⟧{N,γ} }}}.
+  Proof.
+    revert γ c xs.
+    iLöb as "IH".
+    iIntros (γ c xs Φ) "Hstr HΦ".
+    wp_lam.
+    wp_apply (recv_st_spec N loc with "Hstr").
+    iIntros (v) "Hstr".
+    iDestruct "Hstr" as "[Hstr HP]".
+    wp_load.
+    destruct xs.
+    {
+      wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
+      wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
+      eauto 10 with iFrame.
+    }
+    destruct xs.
+    {
+      wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
+      wp_apply (send_st_spec N loc with "[HP Hstr]")=> //. iFrame.
+      eauto 10 with iFrame.
+    }
+    wp_apply (llength_spec (T:=Z))=> //; iIntros (_).
+    wp_pures.
+    assert (bool_decide (S (S (length xs)) ≤ 1) = false) as HSS.
+    { apply bool_decide_false. lia. }
+    rewrite HSS.
+    wp_apply (lsplit_ref_spec with "HP");
+      iIntros (hdy hdz ys zs) "(Heq & Hhdx & Hhdy & Hhdz)".
+    iDestruct "Heq" as %->.
+    wp_apply (new_chan_st_spec N
+               (<!> l @ l ↦ encode ys,
+                <?> l' @ ⌜l = l'⌝ ∗
+                         (∃ ys' : list Z,
+                             l' ↦ encode ys' ∗
+                                ⌜Sorted (≤) ys'⌝ ∗
+                                ⌜Permutation ys' ys⌝),
+                TEnd))=>//;
+             iIntros (cy γy) "[Hstly Hstry]".
+    wp_apply (wp_fork with "[Hstry]").
+    { iNext. iApply ("IH" with "Hstry"). iNext. by iIntros "Hstry". }
+    wp_apply (new_chan_st_spec N
+               (<!> l @ l ↦ encode zs,
+                <?> l' @ ⌜l = l'⌝ ∗
+                         (∃ zs' : list Z,
+                             l' ↦ encode zs' ∗
+                                ⌜Sorted (≤) zs'⌝ ∗
+                                ⌜Permutation zs' zs⌝),
+                TEnd))=>//;
+    iIntros (cz γz) "[Hstlz Hstrz]".
+    wp_apply (wp_fork with "[Hstrz]").
+    { iNext. iApply ("IH" with "Hstrz"). iNext. by iIntros "Hstrz". }
+    wp_apply (send_st_spec N loc with "[Hhdy Hstly]"). iFrame.
+    iIntros "Hstly".
+    wp_apply (send_st_spec N loc with "[Hhdz Hstlz]"). iFrame.
+    iIntros "Hstlz".
+    wp_apply (recv_st_spec N loc with "Hstly").
+    iIntros (ly') "[Hstly Hys']".
+    iDestruct "Hys'" as (<- ys') "(Hys' & Hys'_sorted_of)".
+    iDestruct "Hys'_sorted_of" as %[Hys'_sorted Hys'_perm].
+    wp_apply (recv_st_spec N loc with "Hstlz").
+    iIntros (lz') "[Hstlz Hzs']".
+    iDestruct "Hzs'" as (<- zs') "(Hzs' & Hzs'_sorted_of)".
+    iDestruct "Hzs'_sorted_of" as %[Hzs'_sorted Hzs'_perm].
+    wp_load.
+    wp_load.
+    wp_apply (lmerge_ref_spec with "Hhdx")=> //.
+    iIntros "Hhdx".
+    wp_apply (send_st_spec N loc with "[Hstr Hhdx]").
+    {
+      iFrame.
+      iSplit=> //.
+      iExists (list_merge (≤) ys' zs').
+      iSplit=> //.
+      iPureIntro.
+      split.
+      - apply Sorted_list_merge=> //.
+        { intros x y. lia. }    (* Why is this needed? *)
+      - rewrite merge_Permutation.
+        by apply Permutation_app.
+    }
+    iIntros "Hstr".
+    by iApply "HΦ".
+  Qed.
+
+  Definition list_sort : val :=
+    λ: "xs",
+    let: "c" := new_chan #() in
+    Fork(list_sort_service "c");;
+    send "c" #Left "xs";;
+    recv "c" #Left.
+
+  Lemma list_sort_spec l xs :
+    {{{ l ↦ encode xs }}}
+      list_sort #l
+    {{{ ys, RET #l; l ↦ encode ys ∗ ⌜Sorted (≤) ys⌝ ∗ ⌜Permutation ys xs⌝ }}}.
+  Proof.
+     iIntros (Φ) "Hc HΦ".
+     wp_lam.
+     wp_apply (new_chan_st_spec N
+                 (<!> l @ l ↦ encode xs,
+                  <?> l' @ ⌜l = l'⌝ ∗
+                           (∃ ys : list Z,
+                               l' ↦ encode ys ∗
+                                  ⌜Sorted (≤) ys⌝ ∗
+                                  ⌜Permutation ys xs⌝), TEnd))=>//.
+     iIntros (c γ) "[Hstl Hstr]".
+     wp_apply (wp_fork with "[Hstr]").
+     {
+       iApply (list_sort_service_spec γ c xs with "[Hstr]"). iFrame.
+       iNext. iNext. iIntros "Hstr". done.
+     }
+     wp_apply (send_st_spec N loc with "[Hc $Hstl]"). iFrame.
+     iIntros "Hstl".
+     wp_apply (recv_st_spec N loc with "Hstl").
+     iIntros (v) "[Hstl HP]".
+     iDestruct "HP" as (<- ys) "[Hys Hys_sorted_of]".
+     iApply "HΦ". iFrame.
+  Qed.
+
+End ListSortExample.