diff --git a/_CoqProject b/_CoqProject
index be0b3c395cd761abfa6678daf0db5a88b4ccd475..81b76b779cd83b555b86742a0d06225b1e3ffa9a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,4 +39,5 @@ theories/typing/sum.v
 theories/typing/bool.v
 theories/typing/int.v
 theories/typing/function.v
+theories/typing/programs.v
 theories/typing/mem_instructions.v
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 986660f763483601e464dfb79b966b29819b2e7b..5f220417db86f60befdcbc23eb8f971497e8b4e0 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import hoare.
 From lrust.lifetime Require Import borrow.
 From lrust.typing Require Export type.
-From lrust.typing Require Import typing lft_contexts type_context cont_context.
+From lrust.typing Require Import programs lft_contexts type_context cont_context.
 
 Section fn.
   Context `{typeG Σ}.
diff --git a/theories/typing/perm.v b/theories/typing/perm.v
index c097c0fc1f28860f4f1afc2d035d925be1589e0b..da3c647216aff01ff1f6b908c0572468e4505e09 100644
--- a/theories/typing/perm.v
+++ b/theories/typing/perm.v
@@ -3,6 +3,8 @@ From lrust.typing Require Export type.
 From lrust.lang Require Export proofmode notation.
 From lrust.lifetime Require Import borrow frac_borrow.
 
+(* TODO: This is all still using the outdated type system. *)
+
 Section perm.
   Context `{typeG Σ}.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
new file mode 100644
index 0000000000000000000000000000000000000000..0034b1835b8ca5f6f57c768fda56e20a46f34ad4
--- /dev/null
+++ b/theories/typing/programs.v
@@ -0,0 +1,34 @@
+From iris.program_logic Require Import hoare.
+From iris.base_logic Require Import big_op.
+From lrust.lang Require Export notation memcpy.
+From lrust.typing Require Export type.
+From lrust.typing Require Import perm lft_contexts type_context cont_context.
+From lrust.lang Require Import proofmode.
+From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
+                        (e : expr) : iProp Σ :=
+    (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
+               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
+               WP e {{ _, cont_postcondition }})%I.
+
+  Instance typed_body_llctx_permut E :
+    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
+  Proof.
+    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
+  Qed.
+
+  Instance typed_body_mono E L:
+    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
+  Proof.
+    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
+    iIntros (tid qE) "#LFT HE HL HC HT".
+    iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
+    iApply ("H" with "LFT HE HL [HC] HT").
+    iIntros "HE". by iApply (HC with "LFT HC").
+  Qed.
+
+End typing.
diff --git a/theories/typing/typing.v b/theories/typing/typing.v
index a29d2cc2b0e41371cf7c594dd1f06aef389875eb..3ea3ed1d3935bb4f93ba7c6478a3871adb6c8887 100644
--- a/theories/typing/typing.v
+++ b/theories/typing/typing.v
@@ -6,33 +6,11 @@ From lrust.typing Require Import perm lft_contexts type_context cont_context.
 From lrust.lang Require Import proofmode.
 From lrust.lifetime Require Import frac_borrow reborrow borrow creation.
 
-(* TODO: Split this file into instructions.v and body.v. *)
+(* TODO: This is all still using the outdated type system. *)
 
 Section typing.
   Context `{typeG Σ}.
 
-  Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
-                        (e : expr) : iProp Σ :=
-    (∀ tid qE, lft_ctx -∗ elctx_interp E qE -∗ llctx_interp L 1 -∗
-               (elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
-               WP e {{ _, cont_postcondition }})%I.
-
-  Instance typed_body_llctx_permut E :
-    Proper ((≡ₚ) ==> eq ==> eq ==> eq ==> (⊢)) (typed_body E).
-  Proof.
-    intros L1 L2 HL C ? <- T ? <- e ? <-. rewrite /typed_body. by setoid_rewrite HL.
-  Qed.
-
-  Instance typed_body_mono E L:
-    Proper (flip (cctx_incl E) ==> flip (tctx_incl E L) ==> eq ==> (⊢)) (typed_body E L).
-  Proof.
-    intros C1 C2 HC T1 T2 HT e ? <-. iIntros "H".
-    iIntros (tid qE) "#LFT HE HL HC HT".
-    iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
-    iApply ("H" with "LFT HE HL [HC] HT").
-    iIntros "HE". by iApply (HC with "LFT HC").
-  Qed.
-
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
     ∀ tid, {{ heap_ctx ∗ lft_ctx ∗ ρ tid ∗ na_own tid ⊤ }} e