diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index e06e882765400d9b3241022859efcf1ea0968d7b..bb7cadf6bbb1dac3e786f0714c6a6aa58975946b 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -79,14 +79,17 @@ Notation "'let:' x := e1 'in' e2" :=
 Notation "e1 ;; e2" := (let: <> := e1 in e2)%V
   (at level 100, e2 at level 150, format "e1  ;;  e2") : val_scope.
 
-Notation "e1 'cont:' k xl := e2" :=
-  ((Lam (@cons binder k%RustB nil) e1%E) [Rec k%RustB xl%RustB e2%E])
-  (only parsing, at level 151, k, xl at level 1, e2 at level 150) : expr_scope.
+Notation "'letcont:' k xl := e1 'in' e2" :=
+  ((Lam (@cons binder k%RustB nil) e2%E) [Rec k%RustB xl%RustB e1%E])
+  (at level 102, k, xl at level 1, e1, e2 at level 150) : expr_scope.
+Notation "'withcont:' k1 ':' e1 'cont:' k2 xl := e2" :=
+  ((Lam (@cons binder k1%RustB nil) e1%E) [Rec k2%RustB ((fun _ : eq k1%RustB k2%RustB => xl%RustB) eq_refl) e2%E])
+  (only parsing, at level 151, k1, k2, xl at level 1, e2 at level 150) : expr_scope.
 
 Notation "'call:' f args → k" := (f (@cons expr k args))%E
   (only parsing, at level 102, f, args, k at level 1) : expr_scope.
 Notation "'letcall:' x := f args 'in' e" :=
-  (call: f args → "_k" cont: "_k" [ x ] := e)%E
+  (letcont: "_k" [ x ] := e in call: f args → "_k")%E
   (at level 102, x, f, args at level 1, e at level 150) : expr_scope.
 
 (* RJ: These notations unfortunately do not print.  Also, I don't think
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 8bb2f484540cc3ddf5444a8746329aab261a2d63..b0028a7dcb9c7f8c5adc828487bab27056d9ab4a 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -25,7 +25,7 @@ Section typing.
     □ (∀ k (args : vec val (length argsb)),
           typed_body E L1 (k ◁cont(L1, T') :: C) (T' args)
                      (subst_v (kb::argsb) (k:::args) econt)) -∗
-    typed_body E L2 C T (e2 cont: kb argsb := econt).
+    typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
     iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
     iApply wp_let'; first by rewrite /= decide_left.
@@ -43,7 +43,7 @@ Section typing.
     (∀ k, typed_body E L2 (k ◁cont(L1, T') :: C) T (subst' kb k e2)) -∗
     (∀ k (args : vec val (length argsb)),
           typed_body E L1 C (T' args) (subst_v (kb :: argsb) (k:::args) econt)) -∗
-    typed_body E L2 C T (e2 cont: kb argsb := econt).
+    typed_body E L2 C T (letcont: kb argsb := econt in e2).
   Proof.
     iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid qE) "#LFT Htl HE HL HC HT".
     iApply wp_let'; first by rewrite /= decide_left.
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index afe2a07f780188f5854150841890914b9321e5e1..dedc8131a23577680d9685c14c14c14d8699dc30 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -15,11 +15,12 @@ Section option.
     funrec: <> ["o"] :=
       let: "o'" := !"o" in
       let: "r" := new [ #2 ] in
+    withcont: "k":
       case: !"o'" of
-        [ "r" <-{Σ none} ();; "k" ["r"];
-          "r" <-{Σ some} "o'" +ₗ #1;; "k" ["r"] ]
-      cont: "k" ["r"] :=
-        delete [ #1; "o"];; return: ["r"].
+        [ "r" <-{Σ none} ();; "k" [];
+          "r" <-{Σ some} "o'" +ₗ #1;; "k" [] ]
+    cont: "k" [] :=
+      delete [ #1; "o"];; return: ["r"].
 
   Lemma option_as_mut_type Ï„ :
     typed_val
@@ -27,17 +28,17 @@ Section option.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#". iIntros (α ret p).
       inv_vec p=>o. simpl_subst.
-    iApply (type_cont [_] [] (λ r, [o ◁ _; r!!!0 ◁ _])%TC) ; [solve_typing..| |].
+    iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [] (λ _, [o ◁ _; r ◁ _])%TC) ; [solve_typing..| |].
     - iIntros (k). simpl_subst.
-      iApply type_deref; [solve_typing..|]. iIntros (o'). simpl_subst.
-      iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
       iApply type_case_uniq; [solve_typing..|].
         constructor; last constructor; last constructor; left.
       + iApply (type_sum_unit (option $ &uniq{α}τ)%T); [solve_typing..|].
-        iApply (type_jump [_]); solve_typing.
+        iApply (type_jump []); solve_typing.
       + iApply (type_sum_assign (option $ &uniq{α}τ)%T); [solve_typing..|].
-        iApply (type_jump [_]); solve_typing.
-    - iIntros "/= !#". iIntros (k r). inv_vec r=>r. simpl_subst.
+        iApply (type_jump []); solve_typing.
+    - iIntros "/= !#". iIntros (k args). inv_vec args. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index b208c1968412267f496aeadef41a43cc194636ce..5517099696f5fd0ecba7db2e1c12900d3f272136 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -285,7 +285,8 @@ Section code.
   Definition rc_drop ty : val :=
     funrec: <> ["rc"] :=
       let: "x" := new [ #(option ty).(ty_size) ] in
-      (let: "rc'" := !"rc" in
+    withcont: "k":
+      let: "rc'" := !"rc" in
       let: "count" := !("rc'" +â‚— #0) in
       "rc'" +â‚— #0 <- "count" - #1;;
       if: "count" = #1 then
@@ -296,8 +297,8 @@ Section code.
       else
         "x" <-{Σ none} ();;
         "k" []
-      cont: "k" [] :=
-        delete [ #1; "rc"];; return: ["x"]).
+    cont: "k" [] :=
+      delete [ #1; "rc"];; return: ["x"].
 
   Lemma rc_check_unique ty F tid (l : loc) :
     ↑rc_invN ⊆ F →
@@ -358,7 +359,7 @@ Section code.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (_ ret arg). inv_vec arg=>rcx. simpl_subst.
     iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id (option ty).(ty_size)).
-    iApply (type_cont [] [] (λ r, [rcx ◁ box (uninit 1); x ◁ box (option ty)])%TC) ; [solve_typing..| |]; last first.
+    iApply (type_cont [] [] (λ _, [rcx ◁ box (uninit 1); x ◁ box (option ty)])%TC) ; [solve_typing..| |]; last first.
     { simpl. iAlways. iIntros (k arg). inv_vec arg. simpl_subst.
       iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
@@ -412,7 +413,8 @@ Section code.
   Definition rc_get_mut : val :=
     funrec: <> ["rc"] :=
       let: "x" := new [ #2 ] in
-      (let: "rc'" := !"rc" in
+    withcont: "k":
+      let: "rc'" := !"rc" in
       let: "rc''" := !"rc'" in
       let: "count" := !("rc''" +â‚— #0) in
       if: "count" = #1 then
@@ -421,8 +423,8 @@ Section code.
       else
         "x" <-{Σ none} ();;
         "k" []
-      cont: "k" [] :=
-        delete [ #1; "rc"];; return: ["x"]).
+    cont: "k" [] :=
+      delete [ #1; "rc"];; return: ["x"].
 
   Lemma rc_get_mut_type ty :
     typed_val rc_get_mut (fn(∀ α, [α]; &uniq{α} rc ty) → option (&uniq{α} ty)).
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 95e0224595068cbd4aafb5d9026bc3f419e1d446..0aa1cc24af1b3221c60a27e45ee29b4dec5573be 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -206,6 +206,7 @@ Section ref_functions.
   (* Apply a function within the ref, typically for accessing a component. *)
   Definition ref_map : val :=
     funrec: <> ["ref"; "f"; "env"] :=
+    withcont: "k":
       let: "x'" := !"ref" in
       let: "f'" := !"f" in
       letalloc: "x" <- "x'" in
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 8fd01e4c92119ce900dec8630eee304e539e3839..2854831898b3d3648bb2f7985c2b0b30ee88a991 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -123,11 +123,12 @@ Section refcell_functions.
   Definition refcell_try_borrow : val :=
     funrec: <> ["x"] :=
       let: "r" := new [ #3 ] in
+    withcont: "k":
       let: "x'" := !"x" in
       let: "n" := !"x'" in
       if: "n" ≤ #-1 then
         "r" <-{Σ none} ();;
-        "k" ["r"] (* FIXME RJ: this is very confusing, "k" does not even look like it is bound here... *)
+        "k" []
       else
         "x'" <- "n" + #1;;
         let: "ref" := new [ #2 ] in
@@ -135,21 +136,21 @@ Section refcell_functions.
         "ref" +â‚— #1 <- "x'";;
         "r" <-{2,Σ some} !"ref";;
         delete [ #2; "ref"];;
-        "k" ["r"]
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; return: ["r"].
+        "k" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma refcell_try_borrow_type ty :
     typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box (option (ref α ty))])%TC);
-      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r]; simpl_subst; last first.
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} refcell ty);
+                                    r ◁ box (option (ref α ty))])%TC);
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg]; simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
-    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -167,7 +168,7 @@ Section refcell_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ ref α ty)); [solve_typing..|]; first last.
-      simpl. iApply (type_jump [_]); solve_typing.
+      simpl. iApply (type_jump []); solve_typing.
     - wp_op. wp_write. wp_apply wp_new; [done..|].
       iIntros (lref vl) "(EQ & H† & Hlref)". iDestruct "EQ" as %?%(inj Z.of_nat 2%nat).
       destruct vl as [|?[|?[]]]; try done. wp_let.
@@ -220,13 +221,14 @@ Section refcell_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ ref α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
+      iApply (type_jump []); solve_typing.
   Qed.
 
   (* Unique borrowing. *)
   Definition refcell_try_borrow_mut : val :=
     funrec: <> ["x"] :=
       let: "r" := new [ #3 ] in
+    withcont: "k":
       let: "x'" := !"x" in
       let: "n" := !"x'" in
       if: "n" = #0 then
@@ -236,12 +238,12 @@ Section refcell_functions.
         "ref" +â‚— #1 <- "x'";;
         "r" <-{2,Σ some} !"ref";;
         delete [ #2; "ref"];;
-        "k" ["r"]
+        "k" []
       else
         "r" <-{Σ none} ();;
-        "k" ["r"]
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; return: ["r"].
+        "k" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_val refcell_try_borrow_mut
@@ -249,13 +251,13 @@ Section refcell_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} refcell ty);
-                                    r!!!0 ◁ box (option (refmut α ty))]%TC));
-      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} refcell ty);
+                                    r ◁ box (option (refmut α ty))]%TC));
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
-    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
     iApply type_deref; [solve_typing..|].
     iIntros (x' tid qE) "#LFT Hna HE HL Hk HT". simpl_subst.
     rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -292,7 +294,7 @@ Section refcell_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_memcpy (option $ refmut α ty)); [solve_typing..|].
       simpl. iApply type_delete; [solve_typing..|].
-      iApply (type_jump [_]); solve_typing.
+      iApply (type_jump []); solve_typing.
     - iMod ("Hclose'" with "[Hlx Hownst Hb] Hna") as "[Hβtok Hna]";
         first by iExists st; iFrame.
       iApply (type_type _ _ _
@@ -301,6 +303,6 @@ Section refcell_functions.
       { rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ refmut α ty)); [solve_typing..|].
-      simpl. iApply (type_jump [_]); solve_typing.
+      simpl. iApply (type_jump []); solve_typing.
   Qed.
 End refcell_functions.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 72dd7335d5d45f9d23e775a2633062dcc3833747..85212202feee6bc9f38ba1bc75b2cc9035fb4a8b 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -156,6 +156,7 @@ Section refmut_functions.
   (* Apply a function within the refmut, typically for accessing a component. *)
   Definition refmut_map : val :=
     funrec: <> ["ref"; "f"; "env"] :=
+    withcont: "k":
       let: "x'" := !"ref" in
       let: "f'" := !"f" in
       letalloc: "x" <- "x'" in
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 92ae8769f6a9b7d8624913be9894f6c4c18700c6..f1e5a4044f351016efd4a9be4bb326661f36b1b8 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -123,19 +123,21 @@ Section rwlock_functions.
     funrec: <> ["x"] :=
       let: "r" := new [ #2 ] in
       let: "x'" := !"x" in
-      ("loop" []
-       cont: "loop" [] :=
-         let: "n" := !ˢᶜ"x'" in
-         if: "n" ≤ #-1 then
-           "r" <-{Σ none} ();;
-           "k" ["r"]
-         else
-           if: CAS "x'" "n" ("n" + #1) then
-             "r" <-{Σ some} "x'";;
-             "k" ["r"]
-           else "loop" [])
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; return: ["r"].
+    withcont: "k":
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      let: "n" := !ˢᶜ"x'" in
+        if: "n" ≤ #-1 then
+          "r" <-{Σ none} ();;
+          "k" []
+        else
+          if: CAS "x'" "n" ("n" + #1) then
+            "r" <-{Σ some} "x'";;
+            "k" []
+          else "loop" []
+    cont: "k" [] :=
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlock_try_read_type ty :
     typed_val rwlock_try_read
@@ -143,14 +145,14 @@ Section rwlock_functions.
   Proof.
     intros. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
       iIntros (α ret arg). inv_vec arg=>x. simpl_subst.
-    iApply (type_cont [_] [] (λ r, [x ◁ box (&shr{α} rwlock ty);
-                                    r!!!0 ◁ box (option (rwlockreadguard α ty))])%TC);
-      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg=>r];
+    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
+    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
+    iApply (type_cont [] [] (λ _, [x ◁ box (&shr{α} rwlock ty);
+                                   r ◁ box (option (rwlockreadguard α ty))])%TC);
+      [iIntros (k)|iIntros "/= !#"; iIntros (k arg); inv_vec arg];
       simpl_subst; last first.
     { iApply type_delete; [solve_typing..|].
       iApply (type_jump [_]); solve_typing. }
-    iApply type_new; [solve_typing..|]. iIntros (r). simpl_subst.
-    iApply type_deref; [solve_typing..|]. iIntros (x'). simpl_subst.
     iApply (type_cont [] [] (λ _, [x ◁ _; x' ◁ _; r ◁ _])%TC);
       [iIntros (loop)|iIntros "/= !#"; iIntros (loop arg); inv_vec arg];
       simpl_subst.
@@ -173,7 +175,7 @@ Section rwlock_functions.
       { rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
       iApply (type_sum_unit (option $ rwlockreadguard α ty));
         [solve_typing..|]; first last.
-      simpl. iApply (type_jump [_]); solve_typing.
+      simpl. iApply (type_jump []); solve_typing.
     - wp_op. wp_bind (CAS _ _ _).
       iMod (shr_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose']"; try done.
       iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
@@ -226,7 +228,7 @@ Section rwlock_functions.
           iApply lft_intersect_mono; first done. iApply lft_incl_refl. }
         { rewrite {1}/elctx_interp big_sepL_singleton //. }
         iApply (type_sum_assign (option $ rwlockreadguard α ty)); [solve_typing..|].
-        simpl. iApply (type_jump [_]); solve_typing.
+        simpl. iApply (type_jump []); solve_typing.
       + iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
         iMod ("Hclose'" with "[Hlx Hownst Hst]") as "Hβtok1"; first by iExists _; iFrame.
         iModIntro. iApply (wp_if _ false). iNext.
@@ -241,6 +243,7 @@ Section rwlock_functions.
   (* Acquiring a write lock. *)
   Definition rwlock_try_write : val :=
     funrec: <> ["x"] :=
+    withcont: "k":
       let: "r" := new [ #2 ] in
       let: "x'" := !"x" in
       if: CAS "x'" #0 #(-1) then
@@ -249,8 +252,8 @@ Section rwlock_functions.
       else
         "r" <-{Σ none} ();;
         "k" ["r"]
-      cont: "k" ["r"] :=
-        delete [ #1; "x"];; return: ["r"].
+    cont: "k" ["r"] :=
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlock_try_write_type ty :
     typed_val rwlock_try_write
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 7e353fe1fe5ca4bfb31111f92f7940333df80ab9..76a8a32bd4036fae443757eba587012e49c533a2 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -51,13 +51,14 @@ Section rwlockreadguard_functions.
   Definition rwlockreadguard_drop : val :=
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
-      ("loop" []
-       cont: "loop" [] :=
-         let: "n" := !ˢᶜ"x'" in
-         if: CAS "x'" "n" ("n" - #1) then
-           delete [ #1; "x"];;
-           let: "r" := new [ #0] in return: ["r"]
-         else "loop" []).
+    withcont: "loop":
+      "loop" []
+    cont: "loop" [] :=
+      let: "n" := !ˢᶜ"x'" in
+      if: CAS "x'" "n" ("n" - #1) then
+        delete [ #1; "x"];;
+        let: "r" := new [ #0] in return: ["r"]
+      else "loop" [].
 
   Lemma rwlockreadguard_drop_type ty :
     typed_val rwlockreadguard_drop