diff --git a/_CoqProject b/_CoqProject
index 827b1b793f88b641e917975aa2eee227f485db58..7d1b14e496a9c8fea6565fda216878582bd05c59 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,3 +16,9 @@ theories/examples/sort_br_del.v
 theories/examples/sort_fg.v
 theories/examples/map.v
 theories/examples/map_reduce.v
+theories/logrel/ltyping.v
+theories/logrel/lsty.v
+theories/logrel/session_types.v
+theories/logrel/types.v
+theories/logrel/subtyping.v
+theories/logrel/examples/double.v
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
new file mode 100755
index 0000000000000000000000000000000000000000..64067af89ce69bf7686ea28ce71f1590fd6c1181
--- /dev/null
+++ b/theories/logrel/examples/double.v
@@ -0,0 +1,128 @@
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode lib.par lib.spin_lock.
+From iris.algebra Require Import agree frac csum excl frac_auth.
+From actris.channel Require Import channel proto proofmode.
+From actris.logrel Require Export types subtyping.
+
+Definition prog : val := λ: "c",
+  let: "lock" := newlock #() in
+  let: "p" := (
+    acquire "lock";;
+    let: "x1" := recv "c" in
+    release "lock";;
+    "x1"
+  ) ||| (
+    acquire "lock";;
+    let: "x2" := recv "c" in
+    release "lock";;
+    "x2"
+  ) in "p".
+
+Section GhostState.
+  Class fracG Σ := { frac_inG :> inG Σ fracR }.
+  Definition fracΣ : gFunctors := #[GFunctor fracR].
+  Instance subG_fracΣ {Σ} : subG fracΣ Σ → fracG Σ.
+  Proof. solve_inG. Qed.
+End GhostState.
+
+Section Double.
+  Context `{heapG Σ, chanG Σ, fracG Σ, spawnG Σ}.
+
+  Definition prog_prot : iProto Σ :=
+    (<?> (x : Z), MSG #x; <?> (y : Z), MSG #y; END)%proto.
+
+  Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
+    ((c ↣ prog_prot) ∨
+     (own γ (1/2)%Qp ∗ c ↣ (<?> (x : Z), MSG #x; END)%proto) ∨
+     (own γ 1%Qp ∗ c ↣ END))%I.
+
+  Lemma wp_prog (c : val):
+    {{{ ▷ (c ↣ prog_prot) }}}
+      prog c
+    {{{ v, RET v; ∃ k1 k2 : Z, ⌜v = (#k1, #k2)%V⌝ }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    rewrite /prog.
+    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]".
+    { done. }
+    (* Create lock *)
+    wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
+    { iLeft. iFrame "Hc". }
+    iIntros (lk γlk) "#Hlock".
+    wp_pures.
+    (* Fork into two threads *)
+    wp_bind (par _ _).
+    wp_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
+                with "[Hcredit1] [Hcredit2]").
+    - (* Acquire lock *)
+      wp_apply (acquire_spec with "Hlock").
+      iIntros "[Hlocked Hc]". wp_pures.
+      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
+      + wp_recv (x1) as "_". wp_pures.
+        wp_apply (release_spec with "[Hlocked Hcredit1 Hc]").
+        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit1 Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit2 Hc]".
+        wp_recv (x1) as "_". wp_pures.
+        iCombine "Hcredit1 Hcredit2" as "Hcredit".
+        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit2 Hc]".
+        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
+        done.
+    - (* Acquire lock *)
+      wp_apply (acquire_spec with "Hlock").
+      iIntros "[Hlocked Hc]". wp_pures.
+      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
+      + wp_recv (x1) as "_". wp_pures.
+        wp_apply (release_spec with "[Hlocked Hcredit2 Hc]").
+        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit2 Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit1 Hc]".
+        wp_recv (x1) as "Hx1". wp_pures.
+        iCombine "Hcredit1 Hcredit2" as "Hcredit".
+        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit1 Hc]".
+        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
+        done.
+    - iIntros (x1 x2) "[Hx1 Hx2]".
+      iModIntro. wp_pures.
+      iApply "HΦ".
+      iDestruct "Hx1" as (k1) "->".
+      iDestruct "Hx2" as (k2) "->".
+      by iExists k1, k2.
+  Qed.
+
+  Lemma prog_typed :
+    ⊢ (∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ (lty_int * lty_int))%I.
+  Proof.
+    iIntros (vs) "!> HΓ /=".
+    iApply wp_value.
+    iIntros (c) "Hc".
+    iApply (wp_prog with "[Hc]")=> //=.
+    {
+      iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
+      iApply iProto_le_recv.
+      iIntros "!> !>" (v) ">H !>".
+      iDestruct "H" as (x) "->"=> /=.
+      iExists _. do 2 iSplit=> //.
+      iApply iProto_le_recv.
+      iIntros "!>" (v) ">H !>".
+      iDestruct "H" as (y) "->"=> /=.
+      iExists _. do 2 iSplit=> //.
+      iApply iProto_le_refl.
+    }
+    iIntros "!>" (v) "H".
+    iDestruct "H" as (k1 k2) "->".
+    iExists _, _. iSplit=> //. eauto.
+  Qed.
+
+End Double.
diff --git a/theories/logrel/lsty.v b/theories/logrel/lsty.v
new file mode 100644
index 0000000000000000000000000000000000000000..6f1c5b35199f61689ecfb9c429befe4304fe5833
--- /dev/null
+++ b/theories/logrel/lsty.v
@@ -0,0 +1,46 @@
+From actris.logrel Require Export ltyping.
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import proto proofmode.
+
+Record lsty Σ := Lsty {
+  lsty_car :> iProto Σ;
+}.
+Arguments Lsty {_} _%proto.
+Arguments lsty_car {_} _ : simpl never.
+Bind Scope lsty_scope with lsty.
+Delimit Scope lsty_scope with lsty.
+
+Section lsty_ofe.
+  Context `{Σ : gFunctors}.
+
+  Instance lsty_equiv : Equiv (lsty Σ) :=
+    λ P Q, lsty_car P ≡ lsty_car Q.
+  Instance lsty_dist : Dist (lsty Σ) :=
+    λ n P Q, lsty_car P ≡{n}≡ lsty_car Q.
+
+  Lemma lsty_ofe_mixin : OfeMixin (lsty Σ).
+  Proof. by apply (iso_ofe_mixin (lsty_car : _ → iProto _)). Qed.
+  Canonical Structure lstyO := OfeT (lsty Σ) lsty_ofe_mixin.
+
+  Global Instance lsty_cofe : Cofe lstyO.
+  Proof. by apply (iso_cofe (@Lsty _ : _ → lstyO) lsty_car). Qed.
+
+  Global Instance lsty_inhabited : Inhabited (lsty Σ) :=
+    populate (Lsty inhabitant).
+
+  Global Instance lsty_car_ne : NonExpansive lsty_car.
+  Proof. intros n A A' H. exact H. Qed.
+
+  Global Instance lsty_car_proper : Proper ((≡) ==> (≡)) lsty_car.
+  Proof. intros A A' H. exact H. Qed.
+
+  Global Instance Lsty_ne : NonExpansive Lsty.
+  Proof. solve_proper. Qed.
+
+  Global Instance Lsty_proper : Proper ((≡) ==> (≡)) Lsty.
+  Proof. solve_proper. Qed.
+End lsty_ofe.
+
+Arguments lstyO : clear implicits.
diff --git a/theories/logrel/ltyping.v b/theories/logrel/ltyping.v
new file mode 100755
index 0000000000000000000000000000000000000000..2f00fdc3437a2df742a4f59036ac9607ac8593d2
--- /dev/null
+++ b/theories/logrel/ltyping.v
@@ -0,0 +1,199 @@
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import adequacy notation proofmode.
+
+(* The domain of semantic types: Iris predicates over values *)
+Record lty Σ := Lty {
+  lty_car :> val → iProp Σ;
+}.
+Arguments Lty {_} _%I.
+Arguments lty_car {_} _ _ : simpl never.
+Bind Scope lty_scope with lty.
+Delimit Scope lty_scope with lty.
+
+(* The COFE structure on semantic types *)
+Section lty_ofe.
+  Context `{Σ : gFunctors}.
+
+  (* Equality of semantic types is extensional equality *)
+  Instance lty_equiv : Equiv (lty Σ) := λ A B, ∀ w, A w ≡ B w.
+  Instance lty_dist : Dist (lty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
+
+  (* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
+  Lemma lty_ofe_mixin : OfeMixin (lty Σ).
+  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -d> _)). Qed.
+  Canonical Structure ltyO := OfeT (lty Σ) lty_ofe_mixin.
+
+  Global Instance lty_cofe : Cofe ltyO.
+  Proof. by apply (iso_cofe (@Lty _ : (val -d> _) → ltyO) lty_car). Qed.
+
+  Global Instance lty_inhabited : Inhabited (lty Σ) := populate (Lty inhabitant).
+
+  Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+  Global Instance lty_car_proper : Proper ((≡) ==> (=) ==> (≡)) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+
+  Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
+  Proof. by intros ???. Qed.
+  Global Instance lty_proper : Proper (pointwise_relation _ (≡) ==> (≡)) Lty.
+  Proof. by intros ???. Qed.
+End lty_ofe.
+
+Arguments ltyO : clear implicits.
+
+(* Typing for operators *)
+Class LTyUnboxed {Σ} (A : lty Σ) :=
+  lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝.
+
+Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
+  lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∗ B w.
+
+Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
+  lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∗ B w.
+
+(* Copy types *)
+Class LTyCopy `{invG Σ} (A : lty Σ) :=
+  lty_copy_pers v :> Persistent (A v).
+
+Section Environment.
+  Context `{invG Σ}.
+  Implicit Types A : lty Σ.
+
+  Definition env_ltyped (Γ : gmap string (lty Σ))
+             (vs : gmap string val) : iProp Σ :=
+    ([∗ map] i ↦ A ∈ Γ, ∃ v, ⌜vs !! i = Some v⌝ ∗ lty_car A v)%I.
+
+  Lemma env_ltyped_lookup Γ vs x A :
+    Γ !! x = Some A →
+    env_ltyped Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∗ A v.
+  Proof.
+    iIntros (HΓx) "HΓ".
+    iPoseProof (big_sepM_lookup with "HΓ") as "H"; eauto.
+  Qed.
+
+  Lemma env_ltyped_insert Γ vs x A v :
+    A v -∗ env_ltyped Γ vs -∗
+    env_ltyped (binder_insert x A Γ) (binder_insert x v vs).
+  Proof.
+    destruct x as [|x]=> /=; first by auto.
+    iIntros "HA HΓ".
+    rewrite /env_ltyped.
+    set Γ' := <[x:=A]> Γ.
+    assert (Hx: Γ' !! x = Some A).
+    { apply lookup_insert. }
+    iApply (big_sepM_delete _ _ _ _ Hx).
+    iSplitL "HA".
+    { iExists v. rewrite lookup_insert. auto. }
+    assert (Hsub: delete x Γ' ⊆ Γ).
+    { rewrite delete_insert_delete. apply delete_subseteq. }
+    iPoseProof (big_sepM_subseteq _ _ _ Hsub with "HΓ") as "HΓ".
+    iApply (big_sepM_mono with "HΓ"). simpl.
+    iIntros (y B Hy) "HB".
+    iDestruct "HB" as (w Hw) "HB".
+    iExists w. iFrame. iPureIntro.
+    apply lookup_delete_Some in Hy.
+    destruct Hy as [Hxy _].
+    by rewrite -Hw lookup_insert_ne.
+  Qed.
+
+  Definition env_split (Γ Γ1 Γ2 : gmap string (lty Σ)) : iProp Σ :=
+    □ ∀ vs, env_ltyped Γ vs -∗ env_ltyped Γ1 vs ∗ env_ltyped Γ2 vs.
+
+  Lemma env_split_empty : ⊢ env_split ∅ ∅ ∅.
+  Proof. iIntros (vs) "!> HΓ". rewrite /env_ltyped. auto. Qed.
+
+  Lemma env_split_left Γ Γ1 Γ2 x A:
+    Γ !! x = None →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x := A]> Γ) (<[x := A]> Γ1) Γ2.
+  Proof.
+    iIntros (HΓx) "#Hsplit". iIntros (v) "!> HΓ".
+    iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 $]".
+    iApply (big_sepM_insert_2 with "[Hv]"); simpl; eauto.
+  Qed.
+
+  Lemma env_split_comm Γ Γ1 Γ2:
+    env_split Γ Γ1 Γ2 -∗ env_split Γ Γ2 Γ1.
+  Proof.
+    iIntros "#Hsplit" (vs) "!> HΓ".
+    by iDestruct ("Hsplit" with "HΓ") as "[$ $]".
+  Qed.
+
+  Lemma env_split_right Γ Γ1 Γ2 x A:
+    Γ !! x = None →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x := A]> Γ) Γ1 (<[x := A]> Γ2).
+  Proof.
+    iIntros (HΓx) "Hsplit".
+    iApply env_split_comm. iApply env_split_left; first by assumption.
+    by iApply env_split_comm.
+  Qed.
+
+  (* TODO: Get rid of side condition that x does not appear in Γ *)
+  Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
+    Γ !! x = None →
+    LTyCopy A →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
+  Proof.
+    iIntros (Hcopy HΓx) "#Hsplit". iIntros (vs) "!> HΓ".
+    iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+    iDestruct "Hv" as (v ?) "#HAv".
+    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
+    iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
+  Qed.
+
+  (* TODO: Prove lemmas about this *)
+  Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
+    □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
+
+  Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
+  Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
+
+  Lemma env_copy_extend x A Γ Γ' :
+    Γ !! x = None →
+    env_copy Γ Γ' -∗
+    env_copy (<[x:=A]> Γ) Γ'.
+  Proof.
+    iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+    iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
+    iApply ("Hcopy" with "Hvs").
+  Qed.
+
+  Lemma env_copy_extend_copy x A Γ Γ' :
+    Γ !! x = None →
+    Γ' !! x = None →
+    LTyCopy A →
+    env_copy Γ Γ' -∗
+    env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
+  Proof.
+    iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+    iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
+    iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
+    iDestruct "HA" as (v ?) "#HA".
+    iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
+  Qed.
+End Environment.
+
+(* The semantic typing judgement *)
+Definition ltyped `{!heapG Σ}
+    (Γ : gmap string (lty Σ)) (e : expr) (A : lty Σ) : iProp Σ :=
+  □ ∀ vs, env_ltyped Γ vs -∗ WP subst_map vs e {{ A }}.
+
+Notation "Γ ⊨ e : A" := (ltyped Γ e A)
+  (at level 100, e at next level, A at level 200).
+
+Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
+  (∀ `{heapG Σ}, ∃ A, ⊢ ∅ ⊨ e : A) →
+  rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
+  is_Some (to_val e') ∨ reducible e' σ'.
+Proof.
+  intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
+  destruct (Hty _) as [A He]. iStartProof.
+  iDestruct (He) as "He".
+  iSpecialize ("He" $!∅).
+  iSpecialize ("He" with "[]"); first by rewrite /env_ltyped.
+  iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
+Qed.
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
new file mode 100644
index 0000000000000000000000000000000000000000..00140ce48f8b43471c3b7dfeaa8cdfbb413050dc
--- /dev/null
+++ b/theories/logrel/session_types.v
@@ -0,0 +1,149 @@
+From actris.logrel Require Export ltyping lsty.
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import proto proofmode.
+
+Section protocols.
+  Context `{heapG Σ, protoG Σ}.
+
+  Definition lsty_end : lsty Σ := Lsty END.
+
+  Definition lsty_send (A : lty Σ) (P : lsty Σ) : lsty Σ :=
+    Lsty (<!> v, MSG v {{ A v }}; lsty_car P).
+  Definition lsty_recv (A : lty Σ) (P : lsty Σ) : lsty Σ :=
+    Lsty (<?> v, MSG v {{ A v }}; lsty_car P).
+
+  Definition lsty_branch (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (P1 <&> P2).
+  Definition lsty_select (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (P1 <+> P2).
+
+  Definition lsty_rec1 (C : lsty Σ → lsty Σ)
+             `{!Contractive C}
+             (rec : lsty Σ) : lsty Σ :=
+    Lsty (C rec).
+
+  Instance lsty_rec1_contractive C `{!Contractive C} : Contractive (lsty_rec1 C).
+  Proof. solve_contractive. Qed.
+
+  Definition lsty_rec (C : lsty Σ → lsty Σ) `{!Contractive C} : lsty Σ :=
+    fixpoint (lsty_rec1 C).
+
+  Definition lsty_dual (P : lsty Σ) : lsty Σ :=
+    Lsty (iProto_dual P).
+
+  Definition lsty_app (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (iProto_app P1 P2).
+
+End protocols.
+
+Section Propers.
+  Context `{heapG Σ, protoG Σ}.
+
+  Global Instance lsty_send_ne : NonExpansive2 (@lsty_send Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_send.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+  Qed.
+
+  Global Instance lsty_send_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_send Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_send.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct n as [|n]; try done.
+    apply H1.
+  Qed.
+
+  Global Instance lsty_recv_ne : NonExpansive2 (@lsty_recv Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_recv.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+  Qed.
+
+  Global Instance lsty_recv_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_recv Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_recv.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct n as [|n]; try done.
+    apply H1.
+  Qed.
+
+  Global Instance lsty_branch_ne : NonExpansive2 (@lsty_branch Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_branch.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+    intros v. destruct v; done.
+  Qed.
+
+  Global Instance lsty_branch_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_branch Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_branch.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct v; destruct n as [|n]; try done.
+  Qed.
+
+  Global Instance lsty_select_ne : NonExpansive2 (@lsty_select Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_select.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+    intros v. destruct v; done.
+  Qed.
+
+  Global Instance lsty_select_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_select Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_select.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct v; destruct n as [|n]; try done.
+  Qed.
+
+  Global Instance lsty_dual_ne : NonExpansive (@lsty_dual Σ).
+  Proof.
+    intros n P P' HP.
+    rewrite /lsty_dual.
+    apply Lsty_ne.
+    by apply iProto_dual_ne.
+  Qed.
+
+  Global Instance lsty_app_ne : NonExpansive2 (@lsty_app Σ).
+  Proof.
+    intros n P1 P1' H1 P2 P2' H2.
+    rewrite /lsty_app.
+    apply Lsty_ne.
+    by apply iProto_app_ne.
+  Qed.
+
+End Propers.
+
+Notation "'END'" := lsty_end : lsty_scope.
+Notation "<!!> A ; P" :=
+  (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
+Notation "<??> A ; P" :=
+  (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
+Infix "<+++>" := lsty_select (at level 60) : lsty_scope.
+Infix "<&&&>" := lsty_branch (at level 85) : lsty_scope.
+Infix "<++++>" := lsty_app (at level 60) : lsty_scope.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
new file mode 100644
index 0000000000000000000000000000000000000000..5a71cfc0a3f8a7965f7fa5974fe3ab09c95aedf2
--- /dev/null
+++ b/theories/logrel/subtyping.v
@@ -0,0 +1,312 @@
+From actris.logrel Require Import types.
+From actris.channel Require Import channel.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode.
+
+Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
+  □ ∀ v, (A1 v -∗ A2 v).
+
+Arguments lty_le {_} _%lty _%lty.
+Infix "<:" := lty_le (at level 70).
+Instance: Params (@lty_le) 1 := {}.
+
+Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
+Proof. solve_proper. Qed.
+Instance lty_le_proper {Σ} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ).
+Proof. solve_proper. Qed.
+
+Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
+  â–¡ (iProto_le P1 P2).
+
+Arguments lsty_le {_} _%lsty _%lsty.
+Infix "<p:" := lsty_le (at level 70).
+Instance: Params (@lsty_le) 1 := {}.
+
+Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
+Proof. solve_proper_prepare. f_equiv. solve_proper. Qed.
+Instance lsty_le_proper {Σ} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Section subtype.
+  Context `{heapG Σ, chanG Σ}.
+  Implicit Types A : lty Σ.
+  Implicit Types P : lsty Σ.
+
+  Lemma lty_le_refl A : ⊢ A <: A.
+  Proof. by iIntros (v) "!> H". Qed.
+
+  Lemma lty_le_trans A1 A2 A3 : A1 <: A2 -∗ A2 <: A3 -∗ A1 <: A3.
+  Proof. iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1". Qed.
+
+  Lemma lty_le_copy A : ⊢ copy A <: A.
+  Proof. by iIntros (v) "!> #H". Qed.
+
+  Lemma lty_le_copyable A `{LTyCopy Σ A} : ⊢ A <: copy A.
+  Proof. by iIntros (v) "!> #H". Qed.
+
+  Lemma lty_arr_le A11 A12 A21 A22 :
+    ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
+    (A11 ⊸ A12) <: (A21 ⊸ A22).
+  Proof.
+    iIntros "#H1 #H2" (v) "!> H". iIntros (w) "H'".
+    iApply (wp_step_fupd); first done.
+    { iIntros "!>!>!>". iExact "H2". }
+    iApply (wp_wand with "(H (H1 H'))"). iIntros (v') "H Hle !>".
+    by iApply "Hle".
+  Qed.
+
+  Lemma lty_arr_copy_le A11 A12 A21 A22 :
+    ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
+    (A11 → A12) <: (A21 → A22).
+  Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_arr_le. Qed.
+
+  Lemma lty_prod_le A11 A12 A21 A22 :
+    ▷ (A11 <: A21) -∗ ▷ (A12 <: A22) -∗
+    A11 * A12 <: A21 * A22.
+  Proof.
+    iIntros "#H1 #H2" (v) "!>". iDestruct 1 as (w1 w2 ->) "[H1' H2']".
+    iExists _, _.
+    iDestruct ("H1" with "H1'") as "$".
+    by iDestruct ("H2" with "H2'") as "$".
+  Qed.
+
+  Lemma lty_sum_le A11 A12 A21 A22 :
+    ▷ (A11 <: A21) -∗ ▷ (A12 <: A22) -∗
+    A11 + A12 <: A21 + A22.
+  Proof.
+    iIntros "#H1 #H2" (v) "!> [H | H]"; iDestruct "H" as (w ->) "H".
+    - iDestruct ("H1" with "H") as "H1'". iLeft; eauto.
+    - iDestruct ("H2" with "H") as "H2'". iRight; eauto.
+  Qed.
+
+  Lemma lty_any_le A : ⊢ A <: lty_any.
+  Proof. by iIntros (v) "!> H". Qed.
+
+  Lemma lty_forall_le C1 C2 :
+    ▷ (∀ A, C1 A <: C2 A) -∗
+    (∀ A, C1 A) <: (∀ A, C2 A).
+  Proof.
+    iIntros "#Hle" (v) "!> H". iIntros (w).
+    iApply (wp_step_fupd); first done.
+    { iIntros "!>!>!>". iExact "Hle". }
+    iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
+    by iApply "Hle'".
+  Qed.
+
+  Lemma lty_exist_le C1 C2 :
+    ▷ (∀ A, C1 A <: C2 A) -∗
+    (∃ A, C1 A) <: (∃ A, C2 A).
+  Proof.
+    iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
+  Qed.
+
+  Lemma lty_rec_le_1 (C : lty Σ → lty Σ) `{!Contractive C} :
+    ⊢ lty_rec C <: C (lty_rec C).
+  Proof.
+    rewrite {1}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
+  Qed.
+  Lemma lty_rec_le_2 (C : lty Σ → lty Σ) `{!Contractive C} :
+    ⊢ C (lty_rec C) <: lty_rec C.
+  Proof.
+    rewrite {2}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
+  Qed.
+
+  Lemma lty_rec_le `{Contractive C1, Contractive C2} :
+    (□ ∀ A B, ▷ (A <: B) -∗ C1 A <: C2 B) -∗
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    iIntros "#Hle".
+    iLöb as "IH".
+    iIntros (v) "!> H".
+    rewrite /lty_rec {2}fixpoint_unfold.
+    iEval (rewrite fixpoint_unfold).
+    rewrite {3}/lty_rec_aux {4}/lty_rec_aux.
+    iApply ("Hle" with "[] H").
+    iNext. iApply "IH".
+  Qed.
+
+  Lemma lty_ref_mut_le A1 A2 :
+    ▷ (A1 <: A2) -∗
+    ref_mut A1 <: ref_mut A2.
+  Proof.
+    iIntros "#H1" (v) "!>". iDestruct 1 as (l w ->) "[Hl HA]".
+    iDestruct ("H1" with "HA") as "HA".
+    iExists l, w. by iFrame.
+  Qed.
+
+  Lemma lty_weak_ref_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    ref_shr A1 <: ref_shr A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (l ->) "Hinv".
+    iExists l. iSplit; first done.
+    iApply (inv_iff with "Hinv"). iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
+  Qed.
+
+  Lemma lty_mutex_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    mutex A1 <: mutex A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (N γ l lk ->) "Hinv".
+    rewrite /spin_lock.is_lock.
+    iExists N, γ, l, lk. iSplit; first done.
+    rewrite /spin_lock.is_lock.
+    iDestruct "Hinv" as (l' ->) "Hinv".
+    iExists l'.
+    iSplit; first done.
+    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+  Qed.
+
+  Lemma lty_mutexguard_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    mutexguard A1 <: mutexguard A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>".
+    iDestruct 1 as (N γ l lk w ->) "[Hinv [Hlock Hinner]]".
+    rewrite /spin_lock.is_lock.
+    iExists N, γ, l, lk, w. iSplit; first done.
+    rewrite /spin_lock.is_lock.
+    iFrame "Hlock Hinner".
+    iDestruct "Hinv" as (l' ->) "Hinv".
+    iExists l'.
+    iSplit; first done.
+    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+  Qed.
+
+  Lemma lsty_le_refl P : ⊢ P <p: P.
+  Proof. iApply iProto_le_refl. Qed.
+
+  Lemma lsty_send_le A1 A2 P1 P2 :
+    ▷ (A2 <: A1) -∗ ▷ (P1 <p: P2) -∗
+    (<!!> A1 ; P1) <p: (<!!> A2 ; P2).
+  Proof.
+    iIntros "#HAle #HPle !>".
+    iApply iProto_le_send=> /=.
+    iIntros (x) "H !>".
+    iDestruct ("HAle" with "H") as "H".
+    eauto with iFrame.
+  Qed.
+
+  Lemma lsty_recv_le A1 A2 P1 P2 :
+    ▷ (A1 <: A2) -∗ ▷ (P1 <p: P2) -∗
+    (<??> A1 ; P1) <p: (<??> A2 ; P2).
+  Proof.
+    iIntros "#HAle #HPle !>".
+    iApply iProto_le_recv=> /=.
+    iIntros (x) "H !>".
+    iDestruct ("HAle" with "H") as "H".
+    eauto with iFrame.
+  Qed.
+
+  Lemma lsty_swap_le (A1 A2 : lty Σ) (P : lsty Σ) :
+    ⊢ (<??> A1 ; <!!> A2 ; P) <p: (<!!> A2 ; <??> A1 ; P).
+  Proof.
+    iIntros "!>".
+    iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
+    iExists _, _,
+      (tele_app (TT:=[tele _]) (λ x2, (x2, A2 x2, (P:iProto Σ)))),
+      (tele_app (TT:=[tele _]) (λ x1, (x1, A1 x1, (P:iProto Σ)))),
+    x2, x1.
+    simpl.
+    do 2 (iSplit; [done|]).
+    iFrame "HP1 HP2".
+    iModIntro.
+    do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
+  Qed.
+
+  Lemma lsty_select_le P11 P12 P21 P22 :
+    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
+    (P11 <+++> P12) <p: (P21 <+++> P22).
+  Proof.
+    iIntros "#H1 #H2 !>".
+    rewrite /lsty_select /iProto_branch=> /=.
+    iApply iProto_le_send=> /=.
+    iIntros (x) "_ !>".
+    destruct x; eauto with iFrame.
+  Qed.
+
+  Lemma lsty_branch_le P11 P12 P21 P22 :
+    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
+    (P11 <&&&> P12) <p: (P21 <&&&> P22).
+  Proof.
+    iIntros "#H1 #H2 !>".
+    rewrite /lsty_branch /iProto_branch=> /=.
+    iApply iProto_le_recv=> /=.
+    iIntros (x) "_ !>".
+    destruct x; eauto with iFrame.
+  Qed.
+
+  Lemma lsty_app_le P11 P12 P21 P22 :
+    (P11 <p: P21) -∗ (P12 <p: P22) -∗
+    (P11 <++++> P12) <p: (P21 <++++> P22).
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
+
+  Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
+
+  Lemma lsty_rec_le_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
+    ⊢ lsty_rec C <p: C (lsty_rec C).
+  Proof.
+    rewrite {1}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
+    iApply lsty_le_refl.
+  Qed.
+  Lemma lsty_rec_le_2 (C : lsty Σ → lsty Σ) `{!Contractive C} :
+    ⊢ C (lsty_rec C) <p: lsty_rec C.
+  Proof.
+    rewrite {2}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
+    iApply lsty_le_refl.
+  Qed.
+
+  Lemma lsty_rec_le `{Contractive C1, Contractive C2} :
+    (□ ∀ P P', ▷ (P <p: P') -∗ C1 P <p: C2 P') -∗
+    lsty_rec C1 <p: lsty_rec C2.
+  Proof.
+    iIntros "#Hle".
+    iLöb as "IH".
+    iIntros "!>".
+    rewrite /lsty_rec.
+    iEval (rewrite fixpoint_unfold).
+    iEval (rewrite (fixpoint_unfold (lsty_rec1 C2))).
+    rewrite {1 3}/lsty_rec1.
+    iApply ("Hle" with "[]").
+    iNext. iApply "IH".
+  Qed.
+
+  Lemma lty_chan_le P1 P2 :
+    ▷ (P1 <p: P2) -∗ chan P1 <: chan P2.
+  Proof.
+    iIntros "#Hle" (v) "!> H".
+    iApply (iProto_mapsto_le with "H [Hle]"). eauto.
+  Qed.
+
+  Theorem ltyped_subsumption Γ e τ1 τ2 :
+    τ1 <: τ2 -∗ (Γ ⊨ e : τ1) -∗ (Γ ⊨ e : τ2).
+  Proof.
+    iIntros "#Hle #Hltyped" (vs) "!> Henv".
+    iDestruct ("Hltyped" with "Henv") as "Hltyped'".
+    iApply (wp_wand with "Hltyped' [Hle]").
+    by iIntros (v).
+  Qed.
+
+End subtype.
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
new file mode 100644
index 0000000000000000000000000000000000000000..5ed822d67729f3e213e54b848a361a6e982785b6
--- /dev/null
+++ b/theories/logrel/types.v
@@ -0,0 +1,719 @@
+From actris.logrel Require Export ltyping session_types.
+From actris.channel Require Import proto proofmode.
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode lib.par spin_lock.
+
+Section types.
+  Context `{heapG Σ}.
+
+  Definition lty_unit : lty Σ := Lty (λ w, ⌜ w = #() ⌝%I).
+  Definition lty_bool : lty Σ := Lty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I.
+  Definition lty_int : lty Σ := Lty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
+  Definition lty_copy (A : lty Σ) : lty Σ := Lty (λ w, □ (A w))%I.
+  Definition lty_arr (A1 A2 : lty Σ) : lty Σ := Lty (λ w,
+    ∀ v, ▷ A1 v -∗ WP w v {{ A2 }})%I.
+  (* TODO: Make a non-linear version of prod, using ∧ *)
+  Definition lty_prod (A1 A2 : lty Σ) : lty Σ := Lty (λ w,
+    ∃ w1 w2, ⌜w = (w1,w2)%V⌝ ∗ ▷ A1 w1 ∗ ▷ A2 w2)%I.
+  Definition lty_sum (A1 A2 : lty Σ) : lty Σ := Lty (λ w,
+    (∃ w1, ⌜w = InjLV w1⌝ ∗ ▷ A1 w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∗ ▷ A2 w2))%I.
+  Definition lty_any : lty Σ := Lty (λ w, True%I).
+  Definition lty_rec_aux (C : lty Σ → lty Σ) `{!Contractive C}
+      (rec : lty Σ) : lty Σ := Lty (C rec)%I.
+  Instance lty_rec_aux_contractive C `{!Contractive C} : Contractive (lty_rec_aux C).
+  Proof. solve_contractive. Qed.
+  Definition lty_rec (C : lty Σ → lty Σ) `{!Contractive C} : lty Σ :=
+    fixpoint (lty_rec_aux C).
+  Definition lty_forall (C : lty Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∀ A : lty Σ, WP w #() {{ C A }})%I.
+  Definition lty_forall_lsty (C : lsty Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∀ A : lsty Σ, WP w #() {{ C A }})%I.
+  Definition lty_exist (C : lty Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∃ A : lty Σ, ▷ C A w)%I.
+  Definition lty_exist_lsty (C : lsty Σ → lty Σ) : lty Σ := Lty (λ w,
+    ∃ A : lsty Σ, ▷ C A w)%I.
+  Definition lty_ref_mut (A : lty Σ) : lty Σ := Lty (λ w,
+    ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ A v)%I.
+  Definition ref_shrN := nroot .@ "shr_ref".
+  Definition lty_ref_shr (A : lty Σ) : lty Σ := Lty (λ w,
+    ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ A v))%I.
+  Definition lty_mutex `{lockG Σ} (A : lty Σ) : lty Σ := Lty (λ w,
+    ∃ (N : namespace) (γ : gname) (l : loc) (lk : val),
+      ⌜ w = PairV lk #l ⌝ ∗
+      is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ A v_inner))%I.
+  Definition lty_mutexguard `{lockG Σ} (A : lty Σ) : lty Σ := Lty (λ w,
+    ∃ (N : namespace) (γ : gname) (l : loc) (lk : val) (v : val),
+      ⌜ w = PairV lk #l ⌝ ∗
+      is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ A v_inner) ∗
+      locked γ ∗ l ↦ v)%I.
+  Definition lty_chan `{chanG Σ} (P : lsty Σ) : lty Σ := Lty (λ w, w ↣ P)%I.
+End types.
+
+Notation "()" := lty_unit : lty_scope.
+Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
+Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
+Notation "A ⊸ B" := (lty_arr A B) (at level 99, B at level 200, right associativity) : lty_scope.
+Infix "*" := lty_prod : lty_scope.
+Infix "+" := lty_sum : lty_scope.
+Notation any := lty_any.
+Notation "∀ A1 .. An , C" :=
+  (lty_forall (λ A1, .. (lty_forall (λ An, C%lty)) ..)) : lty_scope.
+Notation "∃ A1 .. An , C" :=
+  (lty_exist (λ A1, .. (lty_exist (λ An, C%lty)) ..)) : lty_scope.
+Notation "∀p A1 .. An , C" :=
+  (lty_forall_lsty (λ A1, .. (lty_forall_lsty (λ An, C%lty)) ..))
+  (at level 200, A1 binder, An binder, right associativity,
+  format "'[ ' '[ ' ∀p A1 .. An ']' , '/' C ']'") : lty_scope.
+Notation "∃p A1 .. An , C" :=
+  (lty_exist_lsty (λ A1, .. (lty_exist_lsty (λ An, C%lty)) ..))
+  (at level 200, A1 binder, An binder, right associativity,
+  format "'[ ' '[ ' ∃p A1 .. An ']' , '/' C ']'") : type_scope.
+Notation "'ref_mut' A" := (lty_ref_mut A) (at level 10) : lty_scope.
+Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
+
+Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
+Notation "'mutexguard' A" := (lty_mutexguard A) (at level 10) : lty_scope.
+Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
+
+Instance binder_insert_instance : Insert binder A (gmap string A) :=
+  { insert := binder_insert }.
+
+Section properties.
+  Context `{heapG Σ}.
+  Implicit Types Γ : gmap string (lty Σ).
+
+  (** Basic properties *)
+  Global Instance lty_unit_unboxed : @LTyUnboxed Σ ().
+  Proof. by iIntros (v ->). Qed.
+  Global Instance lty_unit_copy : @LTyCopy Σ _ ().
+  Proof. iIntros (v). apply _. Qed.
+  Global Instance lty_bool_unboxed : @LTyUnboxed Σ lty_bool.
+  Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
+  Global Instance lty_bool_copy : @LTyCopy Σ _ lty_bool.
+  Proof. iIntros (v). apply _. Qed.
+  Global Instance lty_int_unboxed : @LTyUnboxed Σ lty_int.
+  Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
+  Global Instance lty_int_copy : @LTyCopy Σ _ lty_int.
+  Proof. iIntros (v). apply _. Qed.
+
+  Lemma ltyped_unit Γ : ⊢ Γ ⊨ #() : ().
+  Proof. iIntros "!>" (vs) "_ /=". by iApply wp_value. Qed.
+  Lemma ltyped_bool Γ (b : bool) : ⊢ Γ ⊨ #b : lty_bool.
+  Proof. iIntros "!>" (vs) "_ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed.
+  Lemma ltyped_nat Γ (n : Z) : ⊢ Γ ⊨ #n : lty_int.
+  Proof. iIntros "!>" (vs) "_ /=". iApply wp_value. rewrite /lty_car /=. eauto. Qed.
+
+  (** Operator Properties *)
+  Global Instance lty_bin_op_eq A : LTyUnboxed A → @LTyBinOp Σ EqOp A A lty_bool.
+  Proof.
+    iIntros (Q v1 v2) "A1 _". rewrite /bin_op_eval /lty_car /=.
+    iDestruct (lty_unboxed with "A1") as %Hunb.
+    rewrite decide_True; last solve_vals_compare_safe.
+    eauto.
+  Qed.
+  Global Instance lty_bin_op_arith op :
+    TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
+                 AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] →
+    @LTyBinOp Σ op lty_int lty_int lty_int.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /lty_car /=; eauto.
+  Qed.
+  Global Instance lty_bin_op_compare op :
+    TCElemOf op [LeOp; LtOp] →
+    @LTyBinOp Σ op lty_int lty_int lty_bool.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /lty_car /=; eauto.
+  Qed.
+  Global Instance lty_bin_op_bool op :
+    TCElemOf op [AndOp; OrOp; XorOp] →
+    @LTyBinOp Σ op lty_bool lty_bool lty_bool.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /lty_car /=; eauto.
+  Qed.
+
+  (** Variable properties *)
+  Lemma ltyped_var Γ (x : string) A :
+    Γ !! x = Some A → ⊢ Γ ⊨ x : A.
+  Proof.
+    iIntros (HΓx) "!>".
+    iIntros (vs) "HΓ /=".
+    iDestruct (env_ltyped_lookup with "HΓ") as (v ->) "HA"; first done.
+    by iApply wp_value.
+  Qed.
+
+  (** Copy properties *)
+  Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ).
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_copy_copy A : LTyCopy (copy A).
+  Proof. iIntros (v). apply _. Qed.
+
+  (** Arrow properties *)
+  Global Instance lty_arr_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
+  Proof.
+    intros A A' ? B B' ?.
+    apply lty_ne.
+    intros f.
+    f_equiv.
+    intros w.
+    f_equiv.
+    - by f_contractive.
+    - apply wp_contractive.
+      { apply _. }
+      intros q.
+      destruct n as [|n'].
+      + done.
+      + by simpl.
+  Qed.
+
+  Global Instance lty_arr_ne : NonExpansive2 (@lty_arr Σ _).
+  Proof. solve_proper. Qed.
+
+  Lemma ltyped_app Γ Γ1 Γ2 e1 e2 A1 A2 :
+    env_split Γ Γ1 Γ2 -∗
+    (Γ1 ⊨ e1 : A1 ⊸ A2) -∗ (Γ2 ⊨ e2 : A1) -∗
+    Γ ⊨ e1 e2 : A2.
+  Proof.
+    iIntros "#Hsplit #H1 #H2". iIntros (vs) "!> HΓ /=".
+    iDestruct ("Hsplit" with "HΓ") as "HΓ".
+    iMod (fupd_mask_mono with "HΓ") as "[HΓ1 HΓ2]"; first done.
+    wp_apply (wp_wand with "(H2 [HΓ2 //])"). iIntros (v) "HA1".
+    wp_apply (wp_wand with "(H1 [HΓ1 //])"). iIntros (f) "Hf".
+    iApply ("Hf" $! v with "HA1").
+  Qed.
+
+  Lemma ltyped_lam Γ x e A1 A2 :
+    (binder_insert x A1 Γ ⊨ e : A2) -∗
+    Γ ⊨ (λ: x, e) : A1 ⊸ A2.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iIntros (v) "HA1". wp_pures.
+    iDestruct ("He" $!((binder_insert x v vs)) with "[HΓ HA1]") as "He'".
+    { iApply (env_ltyped_insert with "[HA1 //] [HΓ //]"). }
+    destruct x as [|x]; rewrite /= -?subst_map_insert //.
+  Qed.
+
+  Lemma ltyped_let Γ Γ1 Γ2 (x : binder) e1 e2 A1 A2 :
+    env_split Γ Γ1 Γ2 -∗
+    (Γ1 ⊨ e1 : A1) -∗ (<[x:=A1]>Γ2 ⊨ e2 : A2) -∗
+    Γ ⊨ (let: x:=e1 in e2) : A2.
+  Proof.
+    iIntros "#Hsplit #HA1 #HA2".
+    iApply (ltyped_app Γ Γ2 Γ1 _ _ A1 A2)=> //.
+    - by iApply env_split_comm.
+    - by iApply ltyped_lam=> //=.
+  Qed.
+
+  Lemma ltyped_rec Γ Γ' f x e A1 A2:
+    env_copy Γ Γ' -∗
+    (<[f:=(A1 → A2)%lty]>(<[x:=A1]>Γ') ⊨ e : A2) -∗
+    Γ ⊨ (rec: f x := e) : A1 → A2.
+  Proof.
+    iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
+    iDestruct ("Hcopy" with "HΓ") as "HΓ".
+    iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
+    iModIntro. iLöb as "IH".
+    iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
+    iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
+                  with "[HΓ HA1]") as "He'".
+    { iApply (env_ltyped_insert with "IH").
+      iApply (env_ltyped_insert with "HA1 HΓ"). }
+    destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
+    destruct (decide (x = f)) as [->|].
+    - by rewrite subst_subst delete_idemp insert_insert -subst_map_insert.
+    - rewrite subst_subst_ne // -subst_map_insert.
+      by rewrite -delete_insert_ne // -subst_map_insert.
+  Qed.
+
+  (** Product properties  *)
+  Global Instance lty_prod_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 * A2).
+  Proof. iIntros (v). apply _. Qed.
+  Global Instance lty_prod_contractive n:
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_prod_ne : NonExpansive2 (@lty_prod Σ).
+  Proof. solve_proper. Qed.
+
+  Lemma ltyped_pair Γ Γ1 Γ2 e1 e2 A1 A2 :
+    env_split Γ Γ1 Γ2 -∗
+    (Γ1 ⊨ e1 : A1) -∗ (Γ2 ⊨ e2 : A2) -∗
+    Γ ⊨ (e1,e2) : A1 * A2.
+  Proof.
+    iIntros "#Hsplit #H1 #H2". iIntros (vs) "!> HΓ /=". iApply wp_fupd.
+    iDestruct ("Hsplit" with "HΓ") as "HΓ".
+    iMod (fupd_mask_mono with "HΓ") as "[HΓ1 HΓ2]"; first done.
+    wp_apply (wp_wand with "(H2 [HΓ2 //])"); iIntros (w2) "HA2".
+    wp_apply (wp_wand with "(H1 [HΓ1 //])"); iIntros (w1) "HA1".
+    wp_pures. iExists w1, w2. by iFrame.
+  Qed.
+
+  Definition split : val := λ: "pair" "f", "f" (Fst "pair") (Snd "pair").
+
+  Lemma ltyped_split A1 A2 B:
+    ⊢ ∅ ⊨ split : A1 * A2 → (A1 ⊸ A2 ⊸ B) ⊸ B.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v) "Hv". rewrite /split. wp_pures.
+    iDestruct "Hv" as (w1 w2 ->) "[Hw1 Hw2]".
+    iIntros (f) "Hf". wp_pures.
+    iPoseProof ("Hf" with "Hw1") as "Hf".
+    wp_apply (wp_wand with "Hf").
+    iIntros (g) "Hg". iApply ("Hg" with "Hw2").
+  Qed.
+
+  (** Sum Properties *)
+  Global Instance lty_sum_copy `{!LTyCopy A1, !LTyCopy A2} : LTyCopy (A1 + A2).
+  Proof. iIntros (v). apply _. Qed.
+  Global Instance lty_sum_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_sum Σ).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_sum_ne : NonExpansive2 (@lty_sum Σ).
+  Proof. solve_proper. Qed.
+
+  Lemma ltyped_injl Γ e A1 A2:
+    (Γ ⊨ e : A1) -∗ Γ ⊨ InjL e : A1 + A2.
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(HA [HΓ //])").
+    iIntros (v) "HA'". wp_pures.
+    iLeft. iExists v. auto.
+  Qed.
+
+  Lemma ltyped_injr Γ e A1 A2:
+    (Γ ⊨ e : A2) -∗ Γ ⊨ InjR e : A1 + A2.
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(HA [HΓ //])").
+    iIntros (v) "HA'". wp_pures.
+    iRight. iExists v. auto.
+  Qed.
+
+  Definition paircase : val := λ: "pair" "left" "right",
+    Case "pair" "left" "right".
+
+  Lemma ltyped_paircase A1 A2 B :
+    ⊢ ∅ ⊨ paircase : A1 + A2 → (A1 ⊸ B) ⊸ (A2 ⊸ B) ⊸ B.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    rewrite /paircase. iIntros "!>" (p) "Hp". wp_pures.
+    iIntros (f_left) "Hleft". wp_pures.
+    iIntros (f_right) "Hright". wp_pures.
+    iDestruct "Hp" as "[Hp|Hp]".
+    - iDestruct "Hp" as (w1 ->) "Hp". wp_pures.
+      wp_apply (wp_wand with "(Hleft [Hp //])").
+      iIntros (v) "HB". iApply "HB".
+    - iDestruct "Hp" as (w2 ->) "Hp". wp_pures.
+      wp_apply (wp_wand with "(Hright [Hp //])").
+      iIntros (v) "HB". iApply "HB".
+  Qed.
+
+  (** Universal Properties *)
+  Global Instance lty_forall_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance lty_forall_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _).
+  Proof.
+    intros F F' A. apply lty_ne=> w. f_equiv=> B.
+    apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
+    by destruct n as [|n]; simpl.
+  Qed.
+
+  Global Instance lty_forall_lsty_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall_lsty Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance lty_forall_lsty_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall_lsty Σ _).
+  Proof.
+    intros F F' A. apply lty_ne=> w. f_equiv=> B.
+    apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
+    by destruct n as [|n]; simpl.
+  Qed.
+
+  Lemma ltyped_tlam Γ e C :
+    (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (λ: <>, e) : ∀ A, C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros (A) "/=". wp_pures.
+    iApply ("He" $!(_ vs) with "HΓ").
+  Qed.
+  Lemma ltyped_tlam_lsty Γ e C :
+    (∀ A, Γ ⊨ e : C A) -∗ Γ ⊨ (λ: <>, e) : ∀p A, C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures. iIntros (A) "/=". wp_pures.
+    iApply ("He" $!(_ vs) with "HΓ").
+  Qed.
+
+  Lemma ltyped_tapp Γ e C A :
+    (Γ ⊨ e : ∀ A, C A) -∗ Γ ⊨ e #() : C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB".
+    by iApply ("HB" $! A).
+  Qed.
+  Lemma ltyped_tapp_lsty Γ e C A :
+    (Γ ⊨ e : ∀p A, C A) -∗ Γ ⊨ e #() : C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB".
+    by iApply ("HB" $! A).
+  Qed.
+
+  (** Existential properties *)
+  Global Instance lty_exist_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
+    (LTyCopy (lty_exist C)).
+  Proof. intros v. apply bi.exist_persistent. intros A.
+         apply bi.later_persistent. apply Hcopy. Qed.
+  Global Instance lty_exist_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lty_exist_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ).
+  Proof. solve_contractive. Qed.
+
+  Global Instance lty_exist_lsty_copy C (Hcopy : ∀ A, LTyCopy (C A)) :
+    (LTyCopy (lty_exist_lsty C)).
+  Proof. intros v. apply bi.exist_persistent. intros A.
+         apply bi.later_persistent. apply Hcopy. Qed.
+  Global Instance lty_exist_lsty_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist_lsty Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lty_exist_lsty_contractive n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist_lsty Σ).
+  Proof. solve_contractive. Qed.
+
+  Lemma ltyped_pack Γ e C A :
+    (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃ A, C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB". by iExists A.
+  Qed.
+  Lemma ltyped_pack_lsty Γ e C A :
+    (Γ ⊨ e : C A) -∗ Γ ⊨ e : ∃p A, C A.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "HB". by iExists A.
+  Qed.
+
+  Definition unpack : val := λ: "exist" "f", "f" #() "exist".
+
+  Lemma ltyped_unpack C B :
+    ⊢ ∅ ⊨ unpack : (∃ A, C A) → (∀ A, C A ⊸ B) ⊸ B.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v). iDestruct 1 as (A) "Hv".
+    rewrite /unpack. wp_pures.
+    iIntros (fty) "Hfty". wp_pures.
+    iSpecialize ("Hfty" $! A).
+    wp_bind (fty _). wp_apply (wp_wand with "Hfty").
+    iIntros (f) "Hf".
+    wp_apply (wp_wand with "(Hf [Hv //])").
+    iIntros (w) "HB". iApply "HB".
+  Qed.
+  Lemma ltyped_unpack_lsty C B :
+    ⊢ ∅ ⊨ unpack : (∃p A, C A) → (∀p A, C A ⊸ B) ⊸ B.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v). iDestruct 1 as (A) "Hv".
+    rewrite /unpack. wp_pures.
+    iIntros (fty) "Hfty". wp_pures.
+    iSpecialize ("Hfty" $! A).
+    wp_bind (fty _). wp_apply (wp_wand with "Hfty").
+    iIntros (f) "Hf".
+    wp_apply (wp_wand with "(Hf [Hv //])").
+    iIntros (w) "HB". iApply "HB".
+  Qed.
+
+  (** Mutable Reference properties *)
+  Global Instance lty_ref_mut_contractive : Contractive (@lty_ref_mut Σ _).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_ref_mut_ne : NonExpansive2 (@lty_ref_mut Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance lty_ref_mut_unboxed A : LTyUnboxed (ref_mut A).
+  Proof. iIntros (v). by iDestruct 1 as (i w ->) "?". Qed.
+
+  Definition alloc : val := λ: "init", ref "init".
+  Lemma ltyped_alloc A :
+    ⊢ ∅ ⊨ alloc : A → ref_mut A.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v) "Hv". rewrite /alloc. wp_pures.
+    wp_alloc l as "Hl".
+    iExists l, v. iSplit=> //.
+    iFrame "Hv Hl".
+  Qed.
+
+  (* The intuition for the any is that the value is still there, but
+  it no longer holds any Iris resources. Just as in Rust, where a move
+  might turn into a memcpy, which leaves the original memory
+  unmodified, but moves the resources, in the sense that you can no
+  longer use the memory at the old location. *)
+  Definition load : val := λ: "r", (!"r", "r").
+  Lemma ltyped_load A :
+    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut any.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
+    iDestruct "Hv" as (l w ->) "[Hl Hw]".
+    wp_load. wp_pures.
+    iExists w, #l. iSplit=> //. iFrame "Hw".
+    iExists l, w. iSplit=> //. iFrame "Hl".
+    by iModIntro.
+  Qed.
+
+  Lemma ltyped_load_copy A {copyA : LTyCopy A} :
+    ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A.
+  Proof.
+    iIntros (vs) "!> HΓ /=".
+    iApply wp_value.
+    iIntros "!>" (v) "Hv". rewrite /load. wp_pures.
+    iDestruct "Hv" as (l w ->) "[Hl #Hw]".
+    wp_load. wp_pures.
+    iExists w, #l. iSplit=> //. iFrame "Hw".
+    iExists l, w. iSplit=> //. iFrame "Hl".
+    by iModIntro.
+  Qed.
+
+  Definition store : val := λ: "r" "new", "r" <- "new";; "r".
+
+  Lemma ltyped_store A B:
+    ⊢ ∅ ⊨ store : ref_mut A → B ⊸ ref_mut B.
+  Proof.
+    iIntros (vs) "!> HΓ /=". iApply wp_value.
+    iIntros "!>" (v) "Hv". rewrite /store. wp_pures.
+    iDestruct "Hv" as (l old ->) "[Hl Hold]".
+    iIntros (new) "Hnew". wp_store.
+    iExists l, new. eauto with iFrame.
+  Qed.
+
+  (** Weak Reference properties *)
+  Global Instance lty_ref_shr_contractive : Contractive (@lty_ref_shr Σ _).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_ref_shr_ne : NonExpansive2 (@lty_ref_shr Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance lty_ref_shr_unboxed A : LTyUnboxed (ref_shr A).
+  Proof. iIntros (v). by iDestruct 1 as (l ->) "?". Qed.
+  Global Instance lty_ref_shr_copy A : LTyCopy (ref_shr A).
+  Proof. iIntros (v). apply _. Qed.
+
+  Definition fetch_and_add : val := λ: "r" "inc", FAA "r" "inc".
+  Lemma ltyped_fetch_and_add:
+    ⊢ ∅ ⊨ fetch_and_add : ref_shr lty_int → lty_int → lty_int.
+  Proof.
+    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iApply wp_fupd. rewrite /fetch_and_add; wp_pures.
+    iDestruct "Hr" as (l ->) "Hr".
+    iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
+    iIntros "!> !>" (inc) "Hinc". wp_pures.
+    iDestruct "Hinc" as %[k ->].
+    iInv (ref_shrN .@ l) as (n) "[>Hl >Hn]" "Hclose".
+    iDestruct "Hn" as %[m ->]. wp_faa.
+    iMod ("Hclose" with "[Hl]") as %_.
+    { iExists #(m + k). iFrame "Hl". by iExists (m + k). }
+    by iExists m.
+  Qed.
+
+  Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} :
+    ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A).
+  Proof.
+    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iApply wp_fupd. rewrite /load; wp_pures.
+    iDestruct "Hr" as (l ->) "Hr".
+    iMod (fupd_mask_mono with "Hr") as "#Hr"; first done.
+    wp_bind (!#l)%E.
+    iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
+    wp_load.
+    iMod ("Hclose" with "[Hl HA]") as "_".
+    { iExists v. iFrame "Hl HA". }
+    iIntros "!>". wp_pures. iIntros "!>".
+    iExists _, _.
+    iSplit; first done.
+    iFrame "HA".
+    iExists _.
+    iSplit; first done.
+    by iFrame "Hr".
+  Qed.
+
+  Lemma ltyped_ref_shrstore (A : lty Σ) :
+    ⊢ ∅ ⊨ store : ref_shr A → A → ref_shr A.
+  Proof.
+    iIntros (vs) "!> _ /=". iApply wp_value. iIntros "!>" (r) "Hr".
+    iApply wp_fupd. rewrite /store; wp_pures.
+    iDestruct "Hr" as (l ->) "#Hr".
+    iIntros "!> !>" (x) "HA". wp_pures.
+    wp_bind (_ <- _)%E.
+    iInv (ref_shrN .@ l) as (v) "[>Hl _]" "Hclose".
+    wp_store. iMod ("Hclose" with "[Hl HA]") as "_".
+    { iExists x. iFrame "Hl HA". }
+    iModIntro. wp_pures. iExists _. iSplit; first done. by iFrame "Hr".
+  Qed.
+
+  Section with_lock.
+    Context `{lockG Σ}.
+
+    (** Mutex properties *)
+    Global Instance lty_mutex_contractive : Contractive (@lty_mutex Σ _ _).
+    Proof. solve_contractive. Qed.
+    Global Instance lty_mutex_ne : NonExpansive (@lty_mutex Σ _ _).
+    Proof. solve_proper. Qed.
+
+    Global Instance lty_mutexguard_contractive : Contractive (@lty_mutexguard Σ _ _).
+    Proof. solve_contractive. Qed.
+    Global Instance lty_mutexguard_ne : NonExpansive (@lty_mutexguard Σ _ _).
+    Proof. solve_proper. Qed.
+
+    Definition mutexalloc : val := λ: "x", (newlock #(), ref "x").
+    Lemma ltyped_mutexalloc A:
+      ⊢ ∅ ⊨ mutexalloc : A → mutex A.
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (v) "Hv". rewrite /mutexalloc. wp_pures.
+      wp_alloc l as "Hl".
+      wp_bind (newlock _).
+      set (N := nroot .@ "makelock").
+      iAssert (∃ inner, l ↦ inner ∗ A inner)%I with "[Hl Hv]" as "Hlock".
+      { iExists v. iFrame "Hl Hv". }
+      wp_apply (newlock_spec with "Hlock").
+      iIntros (lk γ) "Hlock".
+      wp_pures. iExists N, γ, l, lk. iSplit=> //.
+    Qed.
+
+    Definition mutexacquire : val := λ: "x", acquire (Fst "x");; (! (Snd "x"), "x").
+    Lemma ltyped_mutexacquire A:
+      ⊢ ∅ ⊨ mutexacquire : mutex A → A * mutexguard A.
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (m) "Hm". rewrite /mutexacquire. wp_pures.
+      iDestruct "Hm" as (N γ l lk ->) "Hlock".
+      iMod (fupd_mask_mono with "Hlock") as "#Hlock"; first done.
+      wp_bind (acquire _).
+      wp_apply (acquire_spec with "Hlock").
+      iIntros "[Hlocked Hinner]".
+      wp_pures.
+      iDestruct "Hinner" as (v) "[Hl HA]".
+      wp_load. wp_pures.
+      iExists v, (lk, #l)%V. iSplit=> //.
+      iFrame "HA".
+      iExists N, γ, l, lk, v. iSplit=> //.
+      by iFrame "Hl Hlocked Hlock".
+    Qed.
+
+    Definition mutexrelease : val :=
+      λ: "inner" "guard", Snd "guard" <- "inner";; release (Fst "guard");; "guard".
+    Lemma ltyped_mutexrelease A:
+      ⊢ ∅ ⊨ mutexrelease : A → mutexguard A ⊸ mutex A.
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (w1) "Hw1". rewrite /mutexrelease. wp_pures.
+      iIntros (w2) "Hw2". wp_pures.
+      iDestruct "Hw2" as (N γ l lk inner ->) "[#Hlock [Hlocked Hinner]]".
+      wp_store.
+      iAssert (∃ inner : val, l ↦ inner ∗ A inner)%I
+        with "[Hinner Hw1]" as "Hinner".
+      { iExists w1. iFrame "Hinner Hw1". }
+      wp_bind (release _).
+      wp_apply (release_spec γ _ (∃ inner, l ↦ inner ∗ A inner)%I
+                  with "[Hlocked Hinner]").
+      { iFrame "Hlock Hlocked".
+        iDestruct "Hinner" as (v) "[Hl HA]". eauto with iFrame. }
+      iIntros "_". wp_pures.
+      iExists N, γ, l, lk. iSplit=> //.
+    Qed.
+  End with_lock.
+
+  Section with_spawn.
+    Context `{spawnG Σ}.
+
+    (** Parallel composition properties *)
+    Definition parallel : val := λ: "e1" "e2", par "e1" "e2".
+
+    Lemma ltyped_parallel A B:
+      ⊢ ∅ ⊨ parallel : (() ⊸ A) → (() ⊸ B) ⊸ (A * B).
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (fa) "Hfa". rewrite /parallel. wp_pures.
+      iIntros (fb) "Hfb". wp_pures.
+      wp_apply (par_spec A B with "[Hfa] [Hfb]").
+      - by wp_apply "Hfa".
+      - by wp_apply "Hfb".
+      - iIntros (v1 v2) "[HA HB] !>". iExists v1, v2. eauto with iFrame.
+    Qed.
+  End with_spawn.
+
+  Section with_chan.
+    Context `{chanG Σ}.
+
+    Global Instance lty_chan_ne : NonExpansive lty_chan.
+    Proof. solve_proper. Qed.
+
+    Definition chanalloc : val := λ: "u", let: "cc" := new_chan #() in "cc".
+    Lemma ltyped_chanalloc P:
+      ⊢ ∅ ⊨ chanalloc : () → (chan P * chan (lsty_dual P)).
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (u) ">->". rewrite /chanalloc. wp_pures.
+      wp_apply (new_chan_spec with "[//]"); iIntros (c1 c2) "Hp".
+      iDestruct "Hp" as "[Hp1 Hp2]". wp_pures.
+      iExists c1, c2. iSplit=> //. iSplitL "Hp1"; by iModIntro.
+    Qed.
+
+    Definition chansend : val := λ: "chan" "val", send "chan" "val";; "chan".
+    Lemma ltyped_chansend A P:
+      ⊢ ∅ ⊨ chansend : chan (<!!> A; P) → A ⊸ chan P.
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (c) "Hc". rewrite /chansend. wp_pures.
+      iIntros (w) "Hw". wp_pures.
+      wp_send with "[$Hw]". wp_pures. iFrame "Hc".
+    Qed.
+
+    Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
+    Lemma ltyped_chanrecv A P:
+      ⊢ ∅ ⊨ chanrecv : chan (<??> A; P) → A * chan P.
+    Proof.
+      iIntros (vs) "!> HΓ /=". iApply wp_value.
+      iIntros "!>" (c) "Hc". rewrite /chanrecv. wp_pures.
+      wp_recv (v) as "HA". wp_pures.
+      iExists v, c. eauto with iFrame.
+    Qed.
+
+    Definition chanfst : val := λ: "c", send "c" #true;; "c".
+    Lemma ltyped_chanfst P1 P2:
+      ⊢ ∅ ⊨ chanfst : chan (P1 <+++> P2) → chan P1.
+    Proof.
+      iIntros (vs) "!> _ /=". iApply wp_value.
+      iIntros "!>" (c) "Hc". rewrite /chanfst. wp_select.
+      wp_pures. iExact "Hc".
+    Qed.
+
+    Definition chansnd : val := λ: "c", send "c" #false;; "c".
+    Lemma ltyped_chansnd P1 P2:
+      ⊢ ∅ ⊨ chansnd : chan (P1 <+++> P2) → chan P2.
+    Proof.
+      iIntros (vs) "!> _ /=". iApply wp_value.
+      iIntros "!>" (c) "Hc". rewrite /chansnd. wp_select.
+      wp_pures. iExact "Hc".
+    Qed.
+
+    Definition chanbranch : val := λ: "c",
+      let b := recv "c" in if: b then InjL "c" else InjR "c".
+
+    Lemma ltyped_chanbranch P1 P2:
+      ⊢ ∅ ⊨ chanbranch : chan (P1 <&&&> P2) → chan P1 + chan P2.
+    Proof.
+      iIntros (vs) "!> _ /=". iApply wp_value.
+      iIntros "!>" (c) "Hc". rewrite /chanbranch. wp_pures.
+      wp_branch; wp_pures.
+      - iLeft. iExists c. iSplit=> //.
+      - iRight. iExists c. iSplit=> //.
+    Qed.
+
+  End with_chan.
+End properties.