diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index 7e49a86ba527fc3b3962de302ceaa6763f35f688..24d397893f093d9a99b6e1e37d5711cbda4db8e1 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -9,6 +9,9 @@ Section bool.
     {| st_own tid vl := (∃ z:bool, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance bool_send : Send bool.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_bool (b : Datatypes.bool) E L :
     typed_instruction_ty E L [] #b bool.
   Proof.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fa67309162d59341be5407ea3aaf36591f0c69cb..7d8e766ce774420dd33094779df743e68c3499bc 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -18,6 +18,9 @@ Section fn.
     iIntros (A n E tys ty tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
 
+  Global Instance fn_send {A n} E tys ty : Send (@fn A n E tys ty).
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma fn_subtype_ty A n E0 L0 E tys1 tys2 ty1 ty2 :
     (∀ x, Forall2 (subtype (E0 ++ E x) L0) (tys2 x : vec _ _) (tys1 x : vec _ _)) →
     (∀ x, subtype (E0 ++ E x) L0 (ty1 x) (ty2 x)) →
diff --git a/theories/typing/int.v b/theories/typing/int.v
index 88e86c932164c27d3b996b18974c65495395dc84..8a376c8dbe4d506b2f4b98717198b031c396b93e 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -9,6 +9,9 @@ Section int.
     {| st_own tid vl := (∃ z:Z, ⌜vl = [ #z ]⌝)%I |}.
   Next Obligation. iIntros (tid vl) "H". iDestruct "H" as (z) "%". by subst. Qed.
 
+  Global Instance int_send : Send int.
+  Proof. iIntros (tid1 tid2 vl). done. Qed.
+
   Lemma typed_int (z : Z) E L :
     typed_instruction_ty E L [] #z int.
   Proof.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 34bccb465b5dd4a48e7e40af444f68324527665c..f100c005561c2f82cbee47369a1daedebc9f2efc 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -178,6 +178,13 @@ Section type.
       iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op // Qp_div_2.
       iDestruct "Hmt" as "[>% Hmt]". subst. by iApply "Hclose".
   Qed.
+
+  Global Instance ty_of_st_sync st :
+    Send (ty_of_st st) → Sync (ty_of_st st).
+  Proof.
+    iIntros (Hsend κ tid1 tid2 l) "H". iDestruct "H" as (vl) "[Hm Hown]".
+    iExists vl. iFrame "Hm". iNext. by iApply Hsend.
+  Qed.
 End type.
 
 Coercion ty_of_st : simple_type >-> type.