Initial commit.

.gitignore

+*.pdf
+*.aux
+*.log
+*.out
+*.synctex.gz
+*.txss
+*.thm
+*.toc
+*.bbl
+*.blg
+*.bcf
+*.run.xml
+_*_.tex
+**/auto/*.el
+\#*\#
+.\#*
+*~
+*.bak
+*.zip
+*.nav
+*.snm
+*.vrb
+*.fdb_latexmk
+*.fls
+*.vo
+*.glob
+*.v.d
+*.vio
+Makefile.coq*
+*.crashcoqide
+.coqdeps.d
+build-dep
+_opam

Makefile

+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	+@make -f Makefile.coq $@
+
+all: Makefile.coq
+	+@make -f Makefile.coq all
+.PHONY: all
+
+clean: Makefile.coq
+	+@make -f Makefile.coq clean
+	find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache
+.PHONY: clean
+
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+
+# Install build-dependencies
+build-dep/opam: opam Makefile
+	@echo "# Creating build-dep package."
+	@mkdir -p build-dep
+	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Pinning build-dep package." && \
+	  if opam --version | grep "^1\." -q; then \
+	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
+	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
+	  else \
+	    opam install $(OPAMFLAGS) build-dep/; \
+	  fi
+
+# Some files that do *not* need to be forwarded to Makefile.coq
+Makefile: ;
+_CoqProject: ;
+opam: ;
+
+# Phony wildcard targets
+phony: ;
+.PHONY: phony

_CoqProject

+-Q theories tutorial_popl20
+# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
+-arg -w -arg -redundant-canonical-projection
+# change_no_check does not exist yet in 8.9.
+-arg -w -arg -convert_concl_no_check
+# "Declare Scope" does not exist yet in 8.9.
+-arg -w -arg -undeclared-scope
+# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
+-arg -w -arg -ambiguous-paths
+
+theories/base.v
+theories/types.v
+theories/typing.v
+theories/sem_types.v
+theories/sem_typing.v
+theories/fundamental.v
+theories/safety.v
+theories/symbol_ghost.v
+theories/unsafe.v

theories/base.v

+From iris.algebra Require Export list gmap.
+From iris.heap_lang Require Export lang notation metatheory.
+
+(** We model type-level lambdas and applications as thunks since heap_lang does
+not have them. *)
+Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing).
+Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
+Notation "'TApp' e" := (App e%E #()) (at level 200, only parsing).
+
+(** We wrap unpack into an explicitly function so that we can have a nice
+notation for it. *)
+Definition exist_unpack : val := λ: "x" "y", "x" "y".
+
+Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (Lam x%binder e2%E) e1%E)
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
+   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
+
+Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E)
+  (at level 200, x at level 1, e1, e2 at level 200, only parsing,
+   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.

theories/fundamental.v

+From tutorial_popl20 Require Export typing sem_typing.
+
+Fixpoint interp `{heapG Σ} (τ : ty) (ρ : list (sem_ty Σ)) : sem_ty Σ :=
+  match τ return _ with
+  | TVar x => default sem_ty_unit (ρ !! x) (* dummy in case [x ∉ ρ] *)
+  | TUnit => sem_ty_unit
+  | TBool => sem_ty_bool
+  | TInt => sem_ty_int
+  | TArr τ1 τ2 => sem_ty_arr (interp τ1 ρ) (interp τ2 ρ)
+  | TProd τ1 τ2 => sem_ty_prod (interp τ1 ρ) (interp τ2 ρ)
+  | TSum τ1 τ2 => sem_ty_sum (interp τ1 ρ) (interp τ2 ρ)
+  | TForall τ => sem_ty_forall (interp τ ∘ (.:: ρ))
+  | TExist τ => sem_ty_exist (interp τ ∘ (.:: ρ))
+  | TRef τ => sem_ty_ref (interp τ ρ)
+  end.
+
+Instance: Params (@interp) 2 := {}.
+Notation interp_env Γ ρ := (flip interp ρ <$> Γ).
+
+Section fundamental.
+  Context `{heapG Σ}.
+  Implicit Types Γ : gmap string ty.
+  Implicit Types ρ : list (sem_ty Σ).
+
+  Global Instance interp_ne τ : NonExpansive (interp τ).
+  Proof. induction τ; solve_proper. Qed.
+  Global Instance interp_proper τ : Proper ((≡) ==> (≡)) (interp τ).
+  Proof. apply ne_proper, _. Qed.
+
+  Lemma interp_env_binder_insert Γ x τ ρ :
+    interp_env (binder_insert x τ Γ) ρ
+    = binder_insert x (interp τ ρ) (interp_env Γ ρ).
+  Proof. destruct x as [|x]=> //=. by rewrite fmap_insert. Qed.
+
+  Lemma interp_ty_lift n τ ρ :
+    n ≤ length ρ →
+    interp (ty_lift n τ) ρ ≡ interp τ (delete n ρ).
+  Proof.
+    (* Use [elim:] instead of [induction] so we can properly name hyps *)
+    revert n ρ. elim: τ; simpl; try (intros; done || f_equiv/=; by auto).
+    - intros x n ρ ?. repeat case_decide; simplify_eq/=; try lia.
+      + by rewrite lookup_delete_lt.
+      + by rewrite lookup_delete_ge; last lia.
+    - intros τ IH n ρ ?. f_equiv=> A /=. naive_solver auto with lia.
+    - intros τ IH n ρ ?. f_equiv=> A /=. naive_solver auto with lia.
+  Qed.
+
+  Lemma interp_env_ty_lift n Γ ρ :
+    n ≤ length ρ →
+    interp_env (ty_lift n <$> Γ) ρ ≡ interp_env Γ (delete n ρ).
+  Proof.
+    intros. rewrite -map_fmap_compose.
+    apply map_fmap_equiv_ext=> x A _ /=. by rewrite interp_ty_lift.
+  Qed.
+
+  Lemma interp_ty_subst i τ τ' ρ :
+    i ≤ length ρ →
+    interp (ty_subst i τ' τ) ρ ≡ interp τ (take i ρ ++ interp τ' ρ :: drop i ρ).
+  Proof.
+    (* Use [elim:] instead of [induction] so we can properly name hyps *)
+    revert i τ' ρ. elim: τ; simpl; try (intros; done || f_equiv/=; by auto).
+    - intros x i τ' ρ ?. repeat case_decide; simplify_eq/=; try lia.
+      + rewrite lookup_app_l; last (rewrite take_length; lia).
+        by rewrite lookup_take; last lia.
+      + by rewrite list_lookup_middle; last (rewrite take_length; lia).
+      + rewrite lookup_app_r; last (rewrite take_length; lia).
+        rewrite take_length lookup_cons_ne_0; last lia.
+        rewrite lookup_drop. do 2 f_equiv; lia.
+    - intros τ IH i τ' ρ ?. f_equiv=> A /=. rewrite IH /=; last lia.
+      by rewrite interp_ty_lift; last lia.
+    - intros τ IH i τ' ρ ?. f_equiv=> A /=. rewrite IH /=; last lia.
+      by rewrite interp_ty_lift; last lia.
+  Qed.
+
+  Instance ty_unboxed_sound τ ρ : ty_unboxed τ → SemTyUnboxed (interp τ ρ).
+  Proof. destruct 1; simpl; apply _. Qed.
+  Instance ty_un_op_sound op τ σ ρ :
+   ty_un_op op τ σ → SemTyUnOp op (interp τ ρ) (interp σ ρ).
+  Proof. destruct 1; simpl; apply _. Qed.
+  Instance ty_bin_op_sound op τ1 τ2 σ ρ :
+   ty_bin_op op τ1 τ2 σ → SemTyBinOp op (interp τ1 ρ) (interp τ2 ρ) (interp σ ρ).
+  Proof. destruct 1; simpl; apply _. Qed.
+
+  Theorem fundamental Γ e τ ρ :
+    (Γ ⊢ₜ e : τ) →
+    interp_env Γ ρ ⊨ e : interp τ ρ.
+  Proof.
+    intros Htyped. iInduction Htyped as [] "IH" forall (ρ); simpl in *.
+    - iApply sem_typed_var. rewrite lookup_fmap. by simplify_option_eq.
+    - iApply sem_typed_unit.
+    - iApply sem_typed_bool.
+    - iApply sem_typed_int.
+    - iApply sem_typed_rec. iSpecialize ("IH" $! ρ).
+      by rewrite !interp_env_binder_insert.
+    - by iApply sem_typed_app.
+    - by iApply sem_typed_pair.
+    - by iApply sem_typed_fst.
+    - by iApply sem_typed_snd.
+    - by iApply sem_typed_injl.
+    - by iApply sem_typed_injr.
+    - by iApply sem_typed_case.
+    - iApply sem_typed_tlam; iIntros (A). iSpecialize ("IH" $! (A :: ρ)).
+      by rewrite interp_env_ty_lift /=; last lia.
+    - rewrite interp_ty_subst /=; last lia.
+      iApply (sem_typed_tapp with "IH").
+    - iApply sem_typed_pack. iSpecialize ("IH" $! ρ).
+      by rewrite interp_ty_subst; last lia.
+    - iApply (sem_typed_unpack with "IH"); iIntros (A).
+      iSpecialize ("IH1" $! (A :: ρ)).
+      rewrite interp_env_binder_insert.
+      rewrite interp_env_ty_lift /=; last lia.
+      by rewrite interp_ty_lift /=; last lia.
+    - by iApply sem_typed_alloc.
+    - by iApply sem_typed_load.
+    - by iApply sem_typed_store.
+    - by iApply sem_typed_faa.
+    - by iApply sem_typed_cmpxchg.
+    - by iApply sem_typed_un_op.
+    - by iApply sem_typed_bin_op.
+    - by iApply sem_typed_if.
+    - by iApply sem_typed_fork.
+  Qed.
+End fundamental.

theories/safety.v

+From tutorial_popl20 Require Export fundamental.
+From iris.heap_lang Require Import adequacy.
+
+Lemma sem_type_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" with "[]"); first by rewrite /env_sem_typed.
+  rewrite subst_map_empty. iApply (wp_wand with "He"); auto.
+Qed.
+
+Lemma type_safety e σ es σ' e' τ :
+  (∅ ⊢ₜ e : τ) →
+  rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
+  is_Some (to_val e') ∨ reducible e' σ'.
+Proof.
+  intros Hty. apply (sem_type_safety (Σ:=heapΣ))=> ?.
+  exists (interp τ []).
+  rewrite (_ : ∅ = interp_env ∅ []); last by rewrite fmap_empty.
+  by apply fundamental.
+Qed.

theories/sem_types.v

+From tutorial_popl20 Require Export base.
+From iris.heap_lang Require Export proofmode.
+From iris.base_logic.lib Require Export invariants.
+
+(* The domain of semantic types: persistent Iris predicates over values *)
+Record sem_ty Σ := SemTy {
+  sem_ty_car :> val → iProp Σ;
+  sem_ty_persistent v : Persistent (sem_ty_car v)
+}.
+Arguments SemTy {_} _%I {_}.
+Arguments sem_ty_car {_} _ _ : simpl never.
+Bind Scope sem_ty_scope with sem_ty.
+Delimit Scope sem_ty_scope with sem_ty.
+Existing Instance sem_ty_persistent.
+
+(* The COFE structure on semantic types *)
+Section sem_ty_cofe.
+  Context `{Σ : gFunctors}.
+
+  Instance sem_ty_equiv : Equiv (sem_ty Σ) := λ A B, ∀ w, A w ≡ B w.
+  Instance sem_ty_dist : Dist (sem_ty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
+  Lemma sem_ty_ofe_mixin : OfeMixin (sem_ty Σ).
+  Proof. by apply (iso_ofe_mixin (sem_ty_car : _ → val -d> _)). Qed.
+  Canonical Structure sem_tyO := OfeT (sem_ty Σ) sem_ty_ofe_mixin.
+  Global Instance sem_ty_cofe : Cofe sem_tyO.
+  Proof.
+    apply (iso_cofe_subtype' (λ A : val -d> iPropO Σ, ∀ w, Persistent (A w))
+      (@SemTy _) sem_ty_car)=> //.
+    - apply _.
+    - apply limit_preserving_forall=> w.
+      by apply bi.limit_preserving_Persistent=> n ??.
+  Qed.
+
+  Global Instance sem_ty_inhabited : Inhabited (sem_ty Σ) := populate (SemTy inhabitant).
+
+  Global Instance sem_ty_car_ne n : Proper (dist n ==> (=) ==> dist n) sem_ty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+  Global Instance sem_ty_car_proper : Proper ((≡) ==> (=) ==> (≡)) sem_ty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+End sem_ty_cofe.
+
+Arguments sem_tyO : clear implicits.
+
+(* The type formers *)
+Section types.
+  Context `{heapG Σ}.
+
+  Definition sem_ty_unit : sem_ty Σ := SemTy (λ w, ⌜ w = #() ⌝)%I.
+  Definition sem_ty_bool : sem_ty Σ := SemTy (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I.
+  Definition sem_ty_int : sem_ty Σ := SemTy (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
+
+  Definition sem_ty_arr (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    □ ∀ v, A1 v -∗ WP App w v {{ A2 }})%I.
+
+  Definition sem_ty_prod (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    ∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ A1 w1 ∧ A2 w2)%I.
+  Definition sem_ty_sum (A1 A2 : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    (∃ w1, ⌜w = InjLV w1⌝ ∧ A1 w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ A2 w2))%I.
+
+  Definition sem_ty_forall (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    □ ∀ A : sem_ty Σ, WP w #() {{ w, C A w }})%I.
+  Definition sem_ty_exist (C : sem_ty Σ → sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    ∃ A : sem_ty Σ, C A w)%I.
+
+  Definition tyN := nroot .@ "ty".
+  Definition sem_ty_ref (A : sem_ty Σ) : sem_ty Σ := SemTy (λ w,
+    ∃ l : loc, ⌜w = #l⌝ ∧ inv (tyN .@ l) (∃ v, l ↦ v ∗ A v))%I.
+End types.
+
+Instance: Params (@sem_ty_arr) 1 := {}.
+Instance: Params (@sem_ty_prod) 1 := {}.
+Instance: Params (@sem_ty_sum) 1 := {}.
+Instance: Params (@sem_ty_forall) 1 := {}.
+Instance: Params (@sem_ty_exist) 1 := {}.
+Instance: Params (@sem_ty_ref) 2 := {}.
+
+(* Nice notations *)
+Notation "()" := sem_ty_unit : sem_ty_scope.
+Infix "→" := sem_ty_arr : sem_ty_scope.
+Infix "*" := sem_ty_prod : sem_ty_scope.
+Infix "+" := sem_ty_sum : sem_ty_scope.
+Notation "∀ A1 .. An , C" :=
+  (sem_ty_forall (λ A1, .. (sem_ty_forall (λ An, C%sem_ty)) ..)) : sem_ty_scope.
+Notation "∃ A1 .. An , C" :=
+  (sem_ty_exist (λ A1, .. (sem_ty_exist (λ An, C%sem_ty)) ..)) : sem_ty_scope.
+Notation "'ref' A" := (sem_ty_ref A) : sem_ty_scope.
+
+Section types_properties.
+  Context `{heapG Σ}.
+
+  (* All type formers are non-expansive *)
+  Global Instance sem_ty_prod_ne : NonExpansive2 (@sem_ty_prod Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_sum_ne : NonExpansive2 (@sem_ty_sum Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_arr_ne : NonExpansive2 (@sem_ty_arr Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_forall_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) (@sem_ty_forall Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_exist_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) (@sem_ty_exist Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_ref_ne : NonExpansive2 (@sem_ty_ref Σ _).
+  Proof. solve_proper. Qed.
+
+  (* All type formers respect setoid equality *)
+  Global Instance sem_ty_prod_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sem_ty_prod Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_sum_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sem_ty_sum Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_arr_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sem_ty_arr Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_forall_proper : Proper (pointwise_relation _ (≡) ==> (≡)) (@sem_ty_forall Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_exist_proper : Proper (pointwise_relation _ (≡) ==>(≡)) (@sem_ty_exist Σ).
+  Proof. solve_proper. Qed.
+  Global Instance sem_ty_ref_proper : Proper ((≡) ==> (≡)) (@sem_ty_ref Σ _).
+  Proof. solve_proper. Qed.
+End types_properties.

theories/sem_typing.v

+From tutorial_popl20 Require Export sem_types.
+
+(* Typing for operators *)
+Class SemTyUnboxed `{heapG Σ} (A : sem_ty Σ) :=
+  sem_ty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝.
+
+Class SemTyUnOp `{heapG Σ} (op : un_op) (A B : sem_ty Σ) :=
+  sem_ty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∧ B w.
+
+Class SemTyBinOp `{heapG Σ} (op : bin_op) (A1 A2 B : sem_ty Σ) :=
+  sem_ty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∧ B w.
+
+(* The semantic typing judgment *)
+Definition env_sem_typed `{heapG Σ} (Γ : gmap string (sem_ty Σ))
+    (vs : gmap string val) : iProp Σ :=
+  ([∗ map] i ↦ A;v ∈ Γ; vs, sem_ty_car A v)%I.
+Instance: Params (@env_sem_typed) 2 := {}.
+Definition sem_typed `{heapG Σ}
+    (Γ : gmap string (sem_ty Σ)) (e : expr) (A : sem_ty Σ) : iProp Σ :=
+  tc_opaque (□ ∀ vs, env_sem_typed Γ vs -∗ WP subst_map vs e {{ A }})%I.
+Instance: Params (@sem_typed) 2 := {}.
+Notation "Γ ⊨ e : A" := (sem_typed Γ e A)
+  (at level 100, e at next level, A at level 200).
+
+Section typed_properties.
+  Context `{heapG Σ}.
+  Implicit Types A B : sem_ty Σ.
+  Implicit Types C : sem_ty Σ → sem_ty Σ.
+
+  Global Instance env_sem_typed_ne n :
+    Proper (dist n ==> (=) ==> dist n) (@env_sem_typed Σ _).
+  Proof. Admitted.
+  Global Instance env_sem_typed_proper :
+    Proper ((≡) ==> (=) ==> (≡)) (@env_sem_typed Σ _).
+  Proof. intros ??????. subst. rewrite /env_sem_typed. Admitted.
+  Global Instance sem_typed_ne n :
+    Proper (dist n ==> (=) ==> dist n ==> dist n) (@sem_typed Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance sem_typed_proper :
+    Proper ((≡) ==> (=) ==> (≡) ==> (≡)) (@sem_typed Σ _).
+  Proof. solve_proper. Qed.
+
+  Global Instance sem_typed_persistent Γ e A : Persistent (Γ ⊨ e : A).
+  Proof. rewrite /sem_typed /=. apply _. Qed.
+
+  (* Environments *)
+  Lemma env_sem_typed_lookup Γ vs x A :
+    Γ !! x = Some A →
+    env_sem_typed Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∧ A v.
+  Proof.
+    iIntros (HΓx) "HΓ". rewrite /env_sem_typed.
+    by iApply (big_sepM2_lookup_1 with "HΓ").
+  Qed.
+  Lemma env_sem_typed_insert Γ vs x A v :
+    A v -∗ env_sem_typed Γ vs -∗
+    env_sem_typed (binder_insert x A Γ) (binder_insert x v vs).
+  Proof.
+    destruct x as [|x]=> /=; first by auto. rewrite /env_sem_typed.
+    iIntros "#HA #HΓ". by iApply (big_sepM2_insert_2 with "[] HΓ").
+  Qed.
+
+  (* Unboxed types *)
+  Global Instance sem_ty_unit_unboxed : SemTyUnboxed ().
+  Proof. by iIntros (v ->). Qed.
+  Global Instance sem_ty_bool_unboxed : SemTyUnboxed sem_ty_bool.
+  Proof. iIntros (v). by iDestruct 1 as (b) "->". Qed.
+  Global Instance sem_ty_int_unboxed : SemTyUnboxed sem_ty_int.
+  Proof. iIntros (v). by iDestruct 1 as (i) "->". Qed.
+  Global Instance sem_ty_ref_unboxed A : SemTyUnboxed (ref A).
+  Proof. iIntros (v). by iDestruct 1 as (i ->) "?". Qed.
+
+  (* Operator typing *)
+  Global Instance sem_ty_un_op_int op : SemTyUnOp op sem_ty_int sem_ty_int.
+  Proof. iIntros (?). iDestruct 1 as (i) "->". destruct op; eauto. Qed.
+  Global Instance sem_ty_un_op_bool : SemTyUnOp NegOp sem_ty_bool sem_ty_bool.
+  Proof. iIntros (?). iDestruct 1 as (i) "->". eauto. Qed.
+
+  Global Instance sem_ty_bin_op_eq A : SemTyUnboxed A → SemTyBinOp EqOp A A sem_ty_bool.
+  Proof.
+    iIntros (? v1 v2) "A1 _". rewrite /bin_op_eval /sem_ty_car /=.
+    iDestruct (sem_ty_unboxed with "A1") as %Hunb.
+    rewrite decide_True; last solve_vals_compare_safe.
+    eauto.
+  Qed.
+  Global Instance sem_ty_bin_op_arith op :
+    TCElemOf op [PlusOp; MinusOp; MultOp; QuotOp; RemOp;
+                 AndOp; OrOp; XorOp; ShiftLOp; ShiftROp] →
+    SemTyBinOp op sem_ty_int sem_ty_int sem_ty_int.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /sem_ty_car /=; eauto.
+  Qed.
+  Global Instance sem_ty_bin_op_compare op :
+    TCElemOf op [LeOp; LtOp] →
+    SemTyBinOp op sem_ty_int sem_ty_int sem_ty_bool.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /sem_ty_car /=; eauto.
+  Qed.
+  Global Instance sem_ty_bin_op_bool op :
+    TCElemOf op [AndOp; OrOp; XorOp] →
+    SemTyBinOp op sem_ty_bool sem_ty_bool sem_ty_bool.
+  Proof.
+    iIntros (? v1 v2); iDestruct 1 as (i1) "->"; iDestruct 1 as (i2) "->".
+    repeat match goal with H : TCElemOf _ _ |- _ => inversion_clear H end;
+      rewrite /sem_ty_car /=; eauto.
+  Qed.
+
+  (* The semantic typing rules *)
+  Lemma sem_typed_var Γ (x : string) A : Γ !! x = Some A → Γ ⊨ x : A.
+  Proof.
+    iIntros (HΓx vs) "!# #HΓ /=".
+    iDestruct (env_sem_typed_lookup with "HΓ") as (v ->) "HA"; first done.
+    by iApply wp_value.
+  Qed.
+
+  Lemma sem_typed_unit Γ : Γ ⊨ #() : ().
+  Proof. iIntros (vs) "!# _ /=". by iApply wp_value. Qed.
+  Lemma sem_typed_bool Γ (b : bool) : Γ ⊨ #b : sem_ty_bool.
+  Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
+  Lemma sem_typed_int Γ (n : Z) : Γ ⊨ #n : sem_ty_int.
+  Proof. iIntros (vs) "!# _ /=". iApply wp_value. rewrite /sem_ty_car /=. eauto. Qed.
+
+  Lemma sem_typed_rec Γ f x e A1 A2 :
+    (binder_insert f (A1 → A2)%sem_ty (binder_insert x A1 Γ) ⊨ e : A2) -∗
+    Γ ⊨ (rec: f x := e) : A1 → A2.
+  Proof.
+    iIntros "#H" (vs) "!# #HΓ /=". wp_pures. iLöb as "IH".
+    iIntros "!#" (v) "#HA1". wp_pures. set (r := RecV f x _).
+    iSpecialize ("H" $! (binder_insert f r (binder_insert x v vs)) with "[#]").
+    { iApply (env_sem_typed_insert with "IH"). by iApply env_sem_typed_insert. }
+    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.
+
+  Lemma sem_typed_app Γ e1 e2 A1 A2 :
+    (Γ ⊨ e1 : A1 → A2) -∗ (Γ ⊨ e2 : A1) -∗ Γ ⊨ e1 e2 : A2.
+  Proof.
+    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
+    wp_apply (wp_wand with "(H2 [//])"); iIntros (w) "#HA1".
+    wp_apply (wp_wand with "(H1 [//])"); iIntros (v) "#HA". by iApply "HA".
+  Qed.
+
+  Lemma sem_typed_pair Γ e1 e2 A1 A2 :
+    (Γ ⊨ e1 : A1) -∗ (Γ ⊨ e2 : A2) -∗ Γ ⊨ (e1,e2) : A1 * A2.
+  Proof.
+    iIntros "#H1 #H2" (vs) "!# #HΓ /=".
+    wp_apply (wp_wand with "(H2 [//])"); iIntros (w2) "#HA2".
+    wp_apply (wp_wand with "(H1 [//])");