diff --git a/_CoqProject b/_CoqProject
index 3c9e5b6bd2011078dd3ee8a48d0906f36d9fd3a5..5bfa8d165dc2f411178584cca3aea05c74afa9ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,3 +27,5 @@ theories/typing/product.v
 theories/typing/sum.v
 theories/typing/uninit.v
 theories/typing/programs.v
+theories/typing/bool.v
+theories/typing/int.v
diff --git a/opam b/opam
index 960bbe4aae8de6774e0fe097967a05d3999f4c1d..3020796f23e6c0a8a92dc22110dd45ee87237e03 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
 depends: [
-  "coq-gpfsl" { (= "dev.2018-04-23.0.2e828a7c") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2018-04-23.3.1dfd6ae7") | (= "dev") }
 ]
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
new file mode 100644
index 0000000000000000000000000000000000000000..74433575c1f2884bf065e6266976dac31f3460d6
--- /dev/null
+++ b/theories/typing/bool.v
@@ -0,0 +1,52 @@
+From lrust.typing Require Export type.
+From lrust.typing Require Import programs.
+Set Default Proof Using "Type".
+
+Section bool.
+  Context `{typeG Σ}.
+
+  Program Definition bool : type :=
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitInt (0|1)) ] => True
+         | _ => False
+         end%I |}.
+  Next Obligation. intros ? [|[| |[[| |[|[]|]]|]] [|]]; auto. Qed.
+  Next Obligation. intros ? [|[| |[[| |[|[]|]]|]] [|]]; apply _. Qed.
+
+  Global Instance bool_wf : TyWf bool := { ty_lfts := []; ty_wf_E := [] }.
+
+  Global Instance bool_send : Send bool.
+  Proof. done. Qed.
+End bool.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
+  Proof.
+    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
+  Qed.
+
+  Lemma type_bool (b : Datatypes.bool) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := #b in e).
+  Proof. iIntros. iApply type_let; [apply type_bool_instr|solve_typing|done]. Qed.
+
+  Lemma type_if E L C T e1 e2 p:
+    p ◁ bool ∈ T →
+    typed_body E L C T e1 -∗ typed_body E L C T e2 -∗
+    typed_body E L C T (if: p then e1 else e2).
+  Proof.
+    iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
+    rewrite !(embed_big_sepL _ T).
+    iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
+    rewrite -!(embed_big_sepL _ T).
+    wp_bind p. iApply (wp_hasty with "Hp").
+    iIntros ([[| |[|[]|]]|]) "_ /="; iIntros ([]); [|]; wp_case.
+    - iApply ("He2" with "LFT HE Htl HL HC HT").
+    - iApply ("He1" with "LFT HE Htl HL HC HT").
+  Qed.
+End typing.
diff --git a/theories/typing/int.v b/theories/typing/int.v
new file mode 100644
index 0000000000000000000000000000000000000000..a41488906deb7b7d7bd2fd6cf3ea4cb72550f91c
--- /dev/null
+++ b/theories/typing/int.v
@@ -0,0 +1,86 @@
+From iris.proofmode Require Import tactics.
+From lrust.typing Require Export type.
+From lrust.typing Require Import bool programs.
+Set Default Proof Using "Type".
+
+Section int.
+  Context `{typeG Σ}.
+
+  Program Definition int : type :=
+    {| st_own tid vl :=
+         match vl return _ with
+         | [ VVal #(LitInt z)] => True
+         | _ => False
+         end%I |}.
+  Next Obligation. intros ? [|[| |[[| |]|]] [|]]; auto. Qed.
+  Next Obligation. intros ? [|[| |[[| |]|]] [|]]; apply _. Qed.
+
+  Global Instance int_wf : TyWf int := { ty_lfts := []; ty_wf_E := [] }.
+
+  Global Instance int_send : Send int.
+  Proof. done. Qed.
+End int.
+
+Section typing.
+  Context `{typeG Σ}.
+
+  Lemma type_int_instr (z : Z) : typed_val #z int.
+  Proof.
+    iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
+    by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_int (z : Z) E L C T x e :
+    Closed (x :b: []) e →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T) (subst' x v e)) -∗
+    typed_body E L C T (let: x := #z in e).
+  Proof. iIntros. iApply type_let; [apply type_int_instr|solve_typing|done]. Qed.
+
+  Lemma type_plus_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 + p2) int.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_plus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 + p2 in e).
+  Proof. iIntros. iApply type_let; [iApply type_plus_instr|solve_typing|done]. Qed.
+
+  Lemma type_minus_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 - p2) int.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op. by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_minus E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ int) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 - p2 in e).
+  Proof. iIntros. iApply type_let; [apply type_minus_instr|solve_typing|done]. Qed.
+
+  Lemma type_le_instr E L p1 p2 :
+    typed_instruction_ty E L [p1 ◁ int; p2 ◁ int] (p1 ≤ p2) bool.
+  Proof.
+    iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
+    wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try iDestruct "H1" as %[].
+    wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try iDestruct "H2" as %[].
+    wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
+  Qed.
+
+  Lemma type_le E L C T T' p1 p2 x e :
+    Closed (x :b: []) e →
+    tctx_extract_ctx E L [p1 ◁ int; p2 ◁ int] T T' →
+    (∀ (v : val), typed_body E L C ((v ◁ bool) :: T') (subst' x v e)) -∗
+    typed_body E L C T (let: x := p1 ≤ p2 in e).
+  Proof. iIntros. iApply type_let; [apply type_le_instr|solve_typing|done]. Qed.
+End typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index fbd892e5f501412bd751f009e04a8d2c60fe8fd9..c13420bd762b2dacc93899f9cb527dc0da3cbbdf 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -1,5 +1,5 @@
 From gpfsl.lang Require Import proofmode.
-From lrust.lang Require Import memcpy.
+From lrust.lang Require Export memcpy.
 From lrust.typing Require Export type lft_contexts type_context cont_context.
 Set Default Proof Using "Type".