diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index f1f858423c57a5614c811069ff13d8479cc3d025..e8d038eb646fe47d103a085ed50db99b806f82ba 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -38,7 +38,7 @@ Definition new_chan : val :=
      let: "lk" := newlock #() in
      ((("l","r"),"lk"), (("r","l"),"lk")).
 
-Definition start_chan : val := λ: "f",
+Definition fork_chan : val := λ: "f",
   let: "cc" := new_chan #() in
   Fork ("f" (Snd "cc"));; Fst "cc".
 
@@ -221,10 +221,10 @@ Section channel.
     - rewrite iProto_pointsto_eq. iExists γ, Right, l, r, lk. by iFrame "Hcr #".
   Qed.
 
-  Lemma start_chan_spec p Φ (f : val) :
+  Lemma fork_chan_spec p Φ (f : val) :
     ▷ (∀ c, c ↣ iProto_dual p -∗ WP f c {{ _, True }}) -∗
     ▷ (∀ c, c ↣ p -∗ Φ c) -∗
-    WP start_chan f {{ Φ }}.
+    WP fork_chan f {{ Φ }}.
   Proof.
     iIntros "Hfork HΦ". wp_lam.
     wp_smart_apply (new_chan_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 71c8b53d66631e9c42a189c1ba160cc3a69dbf85..df1e050e776701a2dddcae8ad114d7d9f96ec9cd 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -489,3 +489,12 @@ Tactic Notation "wp_new_chan" constr(prot) "as"
        "(" simple_intropattern(c1) simple_intropattern(c2) ")" constr(pat) :=
   wp_smart_apply (new_chan_spec prot); [done|];
   iIntros (c1); iIntros (c2); iIntros pat.
+
+Tactic Notation "wp_fork_chan" constr(prot) "as"
+       simple_intropattern(c1) constr(pat1) "and" simple_intropattern(c2) constr(pat2) :=
+  wp_smart_apply (fork_chan_spec prot); [iIntros (c1); iIntros pat1|
+                                         iIntros (c2); iIntros pat2].
+
+Tactic Notation "wp_fork_chan" constr(prot) :=
+  wp_smart_apply (fork_chan_spec prot).
+
diff --git a/theories/examples/basics.v b/theories/examples/basics.v
index ba010b6b865495ee65f51052b664d93375171ee4..71bbf78a4cd6ce3929cd4521f5377238895e7411 100644
--- a/theories/examples/basics.v
+++ b/theories/examples/basics.v
@@ -8,17 +8,17 @@ Local Existing Instance spin_lock.
 
 (** Basic *)
 Definition prog : val := λ: <>,
-  let: "c" := start_chan (λ: "c'", send "c'" #42) in
+  let: "c" := fork_chan (λ: "c'", send "c'" #42) in
   recv "c".
 
 (** Tranfering References *)
 Definition prog_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'", send "c'" (ref #42)) in
+  let: "c" := fork_chan (λ: "c'", send "c'" (ref #42)) in
   ! (recv "c").
 
 (** Delegation, i.e. transfering channels *)
 Definition prog_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     send (Snd "cc2") #42) in
@@ -26,42 +26,42 @@ Definition prog_del : val := λ: <>,
 
 (** Dependent protocols *)
 Definition prog_dep : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "x" := recv "c'" in send "c'" ("x" + #2)) in
   send "c" #40;;
   recv "c".
 
 Definition prog_dep_ref : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := recv "c'" in "l" <- !"l" + #2;; send "c'" #()) in
   let: "l" := ref #40 in send "c" "l";; recv "c";; !"l".
 
 Definition prog_dep_del : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "cc2" := new_chan #() in
     send "c1'" (Fst "cc2");;
     let: "x" := recv (Snd "cc2") in send (Snd "cc2") ("x" + #2)) in
   let: "c2'" := recv "c1" in send "c2'" #40;; recv "c2'".
 
 Definition prog_dep_del_2 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     send (recv "c1'") #40;;
     send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; recv "c1";; recv "c2".
 
 Definition prog_dep_del_3 : val := λ: <>,
-  let: "c1" := start_chan (λ: "c1'",
+  let: "c1" := fork_chan (λ: "c1'",
     let: "c" := recv "c1'" in let: "y" := recv "c1'" in
     send "c" "y";; send "c1'" #()) in
-  let: "c2" := start_chan (λ: "c2'",
+  let: "c2" := fork_chan (λ: "c2'",
     let: "x" := recv "c2'" in send "c2'" ("x" + #2)) in
   send "c1" "c2";; send "c1" #40;; recv "c1";; recv "c2".
 
 (** Loops *)
 Definition prog_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
     let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
   send "c" #18;;
   let: "x1" := recv "c" in
@@ -71,7 +71,7 @@ Definition prog_loop : val := λ: <>,
 
 (** Transfering higher-order functions *)
 Definition prog_fun : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "f" := recv "c'" in send "c'" (λ: <>, "f" #() + #2)) in
   let: "r" := ref #40 in
   send "c" (λ: <>, !"r");;
@@ -79,7 +79,7 @@ Definition prog_fun : val := λ: <>,
 
 (** Lock protected channel endpoints *)
 Definition prog_lock : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     let: "l" := newlock #() in
     Fork (acquire "l";; send "c'" #21;; release "l");;
     acquire "l";; send "c'" #21;; release "l") in
@@ -87,7 +87,7 @@ Definition prog_lock : val := λ: <>,
 
 (** Swapping of sends *)
 Definition prog_swap : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y" := recv "c'" in
     send "c'" ("y" + #2)) in
@@ -95,7 +95,7 @@ Definition prog_swap : val := λ: <>,
   recv "c" + recv "c".
 
 Definition prog_swap_twice : val := λ: <>,
-  let: "c" := start_chan (λ: "c'",
+  let: "c" := fork_chan (λ: "c'",
     send "c'" #20;;
     let: "y1" := recv "c'" in
     let: "y2" := recv "c'" in
@@ -104,7 +104,7 @@ Definition prog_swap_twice : val := λ: <>,
   recv "c" + recv "c".
 
 Definition prog_swap_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
     let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" "c'") in
   send "c" #18;;
   send "c" #20;;
@@ -113,7 +113,7 @@ Definition prog_swap_loop : val := λ: <>,
   "x1" + "x2".
 
 Definition prog_ref_swap_loop : val := λ: <>,
-  let: "c" := start_chan (rec: "go" "c'" :=
+  let: "c" := fork_chan (rec: "go" "c'" :=
      let: "l" := recv "c'" in
      "l" <- !"l" + #2;; send "c'" #();; "go" "c'") in
   let: "l1" := ref #18 in
@@ -209,7 +209,7 @@ Definition prot_swap_loop : iProto Σ :=
 Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot); iIntros (c) "Hc".
   - by wp_send with "[]".
   - wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -217,7 +217,7 @@ Qed.
 Lemma prog_ref_spec : {{{ True }}} prog_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_ref); iIntros (c) "Hc".
   - wp_alloc l as "Hl". by wp_send with "[$Hl]".
   - wp_recv (l) as "Hl". wp_load. by iApply "HΦ".
 Qed.
@@ -225,7 +225,7 @@ Qed.
 Lemma prog_del_spec : {{{ True }}} prog_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_del); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_del); iIntros (c) "Hc".
   - wp_smart_apply (new_chan_spec prot with "[//]").
     iIntros (c2 c2') "[Hc2 Hc2']". wp_send with "[$Hc2]". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -234,7 +234,7 @@ Qed.
 Lemma prog_dep_spec : {{{ True }}} prog_dep #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c) "Hc".
   - wp_recv (x) as "_". by wp_send with "[]".
   - wp_send with "[//]". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -242,7 +242,7 @@ Qed.
 Lemma prog2_ref_spec : {{{ True }}} prog_dep_ref #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_ref); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_ref); iIntros (c) "Hc".
   - wp_recv (l x) as "Hl". wp_load. wp_store. by wp_send with "[Hl]".
   - wp_alloc l as "Hl". wp_send with "[$Hl]". wp_recv as "Hl". wp_load.
     by iApply "HΦ".
@@ -251,7 +251,7 @@ Qed.
 Lemma prog_dep_del_spec : {{{ True }}} prog_dep_del #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del); iIntros (c) "Hc".
   - wp_smart_apply (new_chan_spec prot_dep with "[//]"); iIntros (c2 c2') "[Hc2 Hc2']".
     wp_send with "[$Hc2]". wp_recv (x) as "_". by wp_send with "[]".
   - wp_recv (c2) as "Hc2". wp_send with "[//]". wp_recv as "_".
@@ -261,9 +261,9 @@ Qed.
 Lemma prog_dep_del_2_spec : {{{ True }}} prog_dep_del_2 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del_2); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_2); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
 Qed.
@@ -271,10 +271,10 @@ Qed.
 Lemma prog_dep_del_3_spec : {{{ True }}} prog_dep_del_3 #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_dep_del_3); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_dep_del_3); iIntros (c) "Hc".
   { wp_recv (c2) as "Hc2". wp_recv (y) as "_".
     wp_send with "[//]". by wp_send with "[$Hc2]". }
-  wp_smart_apply (start_chan_spec prot_dep); iIntros (c2) "Hc2".
+  wp_smart_apply (fork_chan_spec prot_dep); iIntros (c2) "Hc2".
   { wp_recv (x) as "_". by wp_send with "[//]". }
   wp_send with "[$Hc2]". wp_send with "[//]".
   wp_recv as "Hc2". wp_recv as "_". by iApply "HΦ".
@@ -283,7 +283,7 @@ Qed.
 Lemma prog_loop_spec : {{{ True }}} prog_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     by wp_smart_apply "IH".
@@ -294,7 +294,7 @@ Qed.
 Lemma prog_fun_spec : {{{ True }}} prog_fun #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_fun); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_fun); iIntros (c) "Hc".
   - wp_recv (P Ψ vf) as "#Hf". wp_send with "[]"; last done.
     iIntros "!>" (Ψ') "HP HΨ'". wp_smart_apply ("Hf" with "HP"); iIntros (x) "HΨ".
     wp_pures. by iApply "HΨ'".
@@ -309,7 +309,7 @@ Lemma prog_lock_spec `{!lockG Σ, contributionG Σ unitUR} :
   {{{ True }}} prog_lock #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec (prot_lock 2)); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec (prot_lock 2)); iIntros (c) "Hc".
   - iMod contribution_init as (γ) "Hs".
     iMod (alloc_client with "Hs") as "[Hs Hcl1]".
     iMod (alloc_client with "Hs") as "[Hs Hcl2]".
@@ -335,7 +335,7 @@ Qed.
 Lemma prog_swap_spec : {{{ True }}} prog_swap #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_swap); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x) as "_". by wp_send with "[//]".
   - wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
@@ -344,7 +344,7 @@ Qed.
 Lemma prog_swap_twice_spec : {{{ True }}} prog_swap_twice #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_swap_twice); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_swap_twice); iIntros (c) "Hc".
   - wp_send with "[//]". wp_recv (x1) as "_". wp_recv (x2) as "_".
     by wp_send with "[//]".
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
@@ -354,7 +354,7 @@ Qed.
 Lemma prog_swap_loop_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
 Proof.
   iIntros (Φ) "_ HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_loop); iIntros (c) "Hc".
   - iLöb as "IH".
     wp_recv (x) as "_". wp_send with "[//]".
     by wp_smart_apply "IH".
@@ -368,7 +368,7 @@ Actris journal paper *)
 Lemma prog_ref_swap_loop_spec : ∀ Φ, Φ #42 -∗ WP prog_ref_swap_loop #() {{ Φ }}.
 Proof.
   iIntros (Φ) "HΦ". wp_lam.
-  wp_smart_apply (start_chan_spec prot_ref_loop); iIntros (c) "Hc".
+  wp_smart_apply (fork_chan_spec prot_ref_loop); iIntros (c) "Hc".
   - iLöb as "IH". wp_lam.
     wp_recv (l x) as "Hl". wp_load. wp_store. wp_send with "[$Hl]".
     by wp_smart_apply "IH".
diff --git a/theories/examples/list_rev.v b/theories/examples/list_rev.v
index 9a121a8964939d36d6b23a1cfc94ab8d12f444bf..70d0adebe7ad2b019b2044a0941043afaa5833cb 100644
--- a/theories/examples/list_rev.v
+++ b/theories/examples/list_rev.v
@@ -9,7 +9,7 @@ Definition list_rev_service : val :=
 
 Definition list_rev_client : val :=
   λ: "l",
-    let: "c" := start_chan list_rev_service in
+    let: "c" := fork_chan list_rev_service in
     send "c" "l";; recv "c".
 
 Section list_rev_example.
@@ -75,7 +75,7 @@ Section list_rev_example.
     {{{ RET #(); llist IT l (reverse xs) }}}.
   Proof.
     iIntros (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec (list_rev_prot)%proto); iIntros (c) "Hc".
     - rewrite -(iProto_app_end_r list_rev_prot).
       iApply (list_rev_service_spec with "Hc"). eauto.
     - iDestruct (iProto_pointsto_le _ _ (list_rev_protI IT) with "Hc []") as "Hc".
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 45692d4af4525226799126b40ae2c7a4d2c5a288..eeb74beddbc1abe9424d1c97bdf663c79f9aaf73 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -60,11 +60,11 @@ Definition par_map_reduce_reduce : val :=
 Definition cmpZfst : val := λ: "x" "y", Fst "x" ≤ Fst "y".
 
 Definition par_map_reduce : val := λ: "n" "m" "map" "red" "xs",
-  let: "cmap" := start_chan (λ: "c", par_map_service "n" "map" "c") in
-  let: "csort" := start_chan (λ: "c", sort_service_fg cmpZfst "c") in
+  let: "cmap" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
+  let: "csort" := fork_chan (λ: "c", sort_service_fg cmpZfst "c") in
   par_map_reduce_map "n" "cmap" "csort" "xs";;
   send "csort" #stop;;
-  let: "cred" := start_chan (λ: "c", par_map_service "m" "red" "c") in
+  let: "cred" := fork_chan (λ: "c", par_map_service "m" "red" "c") in
   (* We need the first sorted element in the loop to compare subsequent elements *)
   if: ~recv "csort" then #() else (* Handle the empty case *)
   let: "jy" := recv "csort" in
@@ -281,10 +281,10 @@ Section mapper.
     {{{ zs, RET #(); ⌜zs ≡ₚ map_reduce map red xs⌝ ∗ llist IC l zs }}}.
   Proof.
     iIntros (??) "#Hmap #Hred !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_smart_apply (start_chan_spec (par_map_protocol IA IZB map n ∅));
+    wp_smart_apply (fork_chan_spec (par_map_protocol IA IZB map n ∅));
       iIntros (cmap) "// Hcmap".
     { wp_pures. wp_smart_apply (par_map_service_spec with "Hmap Hcmap"); auto. }
-    wp_smart_apply (start_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol IZB RZB <++> END)%proto);
       iIntros (csort) "Hcsort".
     { wp_smart_apply (sort_service_fg_spec with "[] Hcsort"); last by auto.
       iApply RZB_cmp_spec. }
@@ -292,7 +292,7 @@ Section mapper.
     wp_smart_apply (par_map_reduce_map_spec with "[$Hl $Hcmap $Hcsort]"); first lia.
     iIntros (iys). rewrite gmultiset_elements_empty right_id_L.
     iDestruct 1 as (Hiys) "[Hl Hcsort] /=". wp_select; wp_pures; simpl.
-    wp_smart_apply (start_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
+    wp_smart_apply (fork_chan_spec (par_map_protocol IZBs IC (uncurry red) m ∅));
       iIntros (cred) "// Hcred".
     { wp_pures. wp_smart_apply (par_map_service_spec with "Hred Hcred"); auto. }
     wp_branch as %_|%Hnil; last first.
diff --git a/theories/examples/par_map.v b/theories/examples/par_map.v
index 525e0e922e0db3d44160cb0977a9428707613cfb..a1bc153d4df7b289279828dea2fb1204738a2d3f 100644
--- a/theories/examples/par_map.v
+++ b/theories/examples/par_map.v
@@ -49,7 +49,7 @@ Definition par_map_client_loop : val :=
       "go" "n" "c" "xs" "ys".
 
 Definition par_map_client : val := λ: "n" "map" "xs",
-  let: "c" := start_chan (λ: "c", par_map_service "n" "map" "c") in
+  let: "c" := fork_chan (λ: "c", par_map_service "n" "map" "c") in
   let: "ys" := lnil #() in
   par_map_client_loop "n" "c" "xs" "ys";;
   lapp "xs" "ys".
@@ -203,7 +203,7 @@ Section map.
     {{{ ys, RET #(); ⌜ys ≡ₚ xs ≫= map⌝ ∗ llist IB l ys }}}.
   Proof.
     iIntros (?) "#Hmap !>"; iIntros (Φ) "Hl HΦ". wp_lam; wp_pures.
-    wp_smart_apply (start_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
+    wp_smart_apply (fork_chan_spec (par_map_protocol n ∅)); iIntros (c) "// Hc".
     { wp_smart_apply (par_map_service_spec with "Hmap Hc"); auto. }
     wp_pures. wp_smart_apply (lnil_spec with "[//]"); iIntros (k) "Hk".
     wp_smart_apply (par_map_client_loop_spec with "[$Hl $Hk $Hc //]"); first lia.
diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index 03f95108f3a2cdff1296b58b201128f59f995a06..4bf819a42397c7730f69ece0477e2e5c8f9b6281 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -24,8 +24,8 @@ Definition sort_service : val :=
     let: "xs" := recv "c" in
     if: llength "xs" ≤ #1 then send "c" #() else
     let: "zs" := lsplit "xs" in
-    let: "cy" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "cz" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "cy" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "cz" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "cy" "xs";;
     send "cz" "zs";;
     recv "cy";; recv "cz";;
@@ -37,7 +37,7 @@ Definition sort_service_func : val := λ: "c",
   sort_service "cmp" "c".
 
 Definition sort_client_func : val := λ: "cmp" "xs",
-  let: "c" := start_chan sort_service_func in
+  let: "c" := fork_chan sort_service_func in
   send "c" "cmp";; send "c" "xs";;
   recv "c".
 
@@ -105,10 +105,10 @@ Section sort.
       wp_send with "[$Hl]"; first by auto. by iApply "HΨ". }
     wp_smart_apply (lsplit_spec with "Hl"); iIntros (l2 vs1 vs2);
       iDestruct 1 as (->) "[Hl1 Hl2]".
-    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
+    wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cy) "Hcy".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply ("IH" with "Hcy"); auto. }
-    wp_smart_apply (start_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
+    wp_smart_apply (fork_chan_spec (sort_protocol I R)); iIntros (cz) "Hcz".
     { rewrite -{2}(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply ("IH" with "Hcz"); auto. }
     wp_send with "[$Hl1]".
@@ -141,7 +141,7 @@ Section sort.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec sort_protocol_func); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec sort_protocol_func); iIntros (c) "Hc".
     { rewrite -(right_id END%proto _ (iProto_dual _)).
       wp_smart_apply (sort_service_func_spec with "Hc"); auto. }
     wp_send with "[$Hcmp]".
diff --git a/theories/examples/sort_br_del.v b/theories/examples/sort_br_del.v
index 10ec01fa2667eaf8bf348033a7d99ef173c1a52c..166a69e1bc7083550f5c5d9a4b30217e2196fb24 100644
--- a/theories/examples/sort_br_del.v
+++ b/theories/examples/sort_br_del.v
@@ -20,7 +20,7 @@ Definition sort_service_br : val :=
 Definition sort_service_del : val :=
   rec: "go" "cmp" "c" :=
     if: ~recv "c" then #() else
-    send "c" (start_chan (λ: "c", sort_service "cmp" "c"));;
+    send "c" (fork_chan (λ: "c", sort_service "cmp" "c"));;
     "go" "cmp" "c".
 
 Definition sort_service_br_del : val :=
@@ -29,7 +29,7 @@ Definition sort_service_br_del : val :=
       sort_service "cmp" "c";;
       "go" "cmp" "c"
     else if: recv "c" then
-      send "c" (start_chan (λ: "c", "go" "cmp" "c"));;
+      send "c" (fork_chan (λ: "c", "go" "cmp" "c"));;
       "go" "cmp" "c"
     else #().
 
@@ -76,7 +76,7 @@ Section sort_service_br_del.
   Proof.
     iIntros "#Hcmp !>" (Ψ) "Hc HΨ". iLöb as "IH" forall (Ψ).
     wp_rec. wp_branch; wp_pures.
-    { wp_smart_apply (start_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
+    { wp_smart_apply (fork_chan_spec (sort_protocol I R <++> END)%proto); iIntros (c') "Hc'".
       { wp_pures. wp_smart_apply (sort_service_spec with "Hcmp Hc'"); auto. }
       wp_send with "[$Hc']". by wp_smart_apply ("IH" with "Hc"). }
     by iApply "HΨ".
@@ -102,7 +102,7 @@ Section sort_service_br_del.
     { wp_smart_apply (sort_service_spec with "Hcmp Hc"); iIntros "Hc".
       by wp_smart_apply ("IH" with "Hc"). }
     wp_branch; wp_pures.
-    { wp_smart_apply (start_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
+    { wp_smart_apply (fork_chan_spec sort_protocol_br_del); iIntros (c') "Hc'".
       { wp_smart_apply ("IH" with "Hc'"); auto. }
       wp_send with "[$Hc']".
       by wp_smart_apply ("IH" with "Hc"). }
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index f657fad94d659d4ccc7b7de13d375ac30872575e..4433d2846ad4029b4c17a572d2e75c043153c00d 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -42,8 +42,8 @@ Definition sort_service_fg : val :=
     let: "x" := recv "c" in
     if: ~(recv "c") then send "c" #cont;; send "c" "x";; send "c" #stop else
     let: "y" := recv "c" in
-    let: "c1" := start_chan (λ: "c", "go" "cmp" "c") in
-    let: "c2" := start_chan (λ: "c", "go" "cmp" "c") in
+    let: "c1" := fork_chan (λ: "c", "go" "cmp" "c") in
+    let: "c2" := fork_chan (λ: "c", "go" "cmp" "c") in
     send "c1" #cont;; send "c1" "x";;
     send "c2" #cont;; send "c2" "y";;
     sort_service_fg_split "c" "c1" "c2";;
@@ -66,7 +66,7 @@ Definition recv_all : val :=
     "go" "c" "ys";; lcons "x" "ys".
 
 Definition sort_client_fg : val := λ: "cmp" "xs",
-  let: "c" := start_chan (λ: "c", sort_service_fg "cmp" "c") in
+  let: "c" := fork_chan (λ: "c", sort_service_fg "cmp" "c") in
   send_all "c" "xs";;
   send "c" #stop;;
   recv_all "c" "xs".
@@ -221,10 +221,10 @@ Section sort_fg.
     wp_rec; wp_pures. wp_branch; wp_pures.
     - wp_recv (x1 v1) as "HIx1". wp_branch; wp_pures.
       + wp_recv (x2 v2) as "HIx2".
-        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cy) "Hcy". wp_smart_apply ("IH" with "Hcy"). auto. }
         iIntros (cy) "Hcy".
-        wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto).
+        wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto).
         { iIntros (cz) "Hcz". wp_smart_apply ("IH" with "Hcz"); auto. }
         iIntros (cz) "Hcz". rewrite !right_id.
         wp_select. wp_send with "[$HIx1]".
@@ -281,7 +281,7 @@ Section sort_fg.
     {{{ ys, RET #(); ⌜Sorted R ys⌝ ∗ ⌜ys ≡ₚ xs⌝ ∗ llist I l ys }}}.
   Proof.
     iIntros "#Hcmp !>" (Φ) "Hl HΦ". wp_lam.
-    wp_smart_apply (start_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
+    wp_smart_apply (fork_chan_spec (sort_fg_protocol <++> END)%proto); iIntros (c) "Hc".
     { wp_smart_apply (sort_service_fg_spec with "Hcmp Hc"); auto. }
     wp_smart_apply (send_all_spec with "[$Hl $Hc]"); iIntros "[Hl Hc]".
     wp_select.
diff --git a/theories/examples/swap_mapper.v b/theories/examples/swap_mapper.v
index 1eb316cead5c7cb49a56e8ed0b173466071caab8..9e9d295d03b76e5fc4a61d7399119febe1424c01 100644
--- a/theories/examples/swap_mapper.v
+++ b/theories/examples/swap_mapper.v
@@ -25,7 +25,7 @@ Definition recv_all : val :=
 
 Definition swap_mapper_client : val :=
   λ: "f" "xs",
-    let: "c" := start_chan (λ: "c", swap_mapper_service "f" "c") in
+    let: "c" := fork_chan (λ: "c", swap_mapper_service "f" "c") in
     let: "n" := llength "xs" in
     send_all "c" "xs";; recv_all "c" "xs" "n";; send "c" #false.
 
@@ -373,7 +373,7 @@ Section with_Σ.
   Proof.
     iIntros "#Hfspec !>" (Φ) "HIT HΦ".
     wp_lam.
-    wp_smart_apply (start_chan_spec mapper_prot); iIntros (c) "// Hc".
+    wp_smart_apply (fork_chan_spec mapper_prot); iIntros (c) "// Hc".
     { wp_lam. rewrite -(iProto_app_end_r (iProto_dual mapper_prot)).
       iApply (swap_mapper_service_spec _ _ END%proto with "Hfspec Hc").
       auto. }