diff --git a/README.md b/README.md
index 3f3d91cb280439eb539b4afa02d9d47001c2f46e..6d6891023d77c8d8599b5aef6ba80ccacda2cde5 100644
--- a/README.md
+++ b/README.md
@@ -91,7 +91,7 @@ borrows" in the Coq development.
 | F-endlft              | programs.v      | type_endlft           |
 | F-call                | function.v      | type_call'            |
 
-Some of these lemmas are called `something'` because the version without the `'` is a derived, more speicalized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
+Some of these lemmas are called `something'` because the version without the `'` is a derived, more specialized form used together with our eauto-based `solve_typing` tactic.  You can see this tactic in action in the [examples](theories/typing/examples) subfolder.
 
 ### Lifetime Logic Rules
 
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 2deec3a41d025ae81a95b0c1260e84c91dc5ad92..de9046c586795650d394acb9017dcd62bbe6144a 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -16,7 +16,7 @@ Section own.
     end%I.
   Next Obligation. intros _ _ _ sz0 ? n ?. by apply Qcmult_pos_pos. Qed.
   Arguments freeable_sz : simpl never.
-  Global Instance freable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
+  Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
 
   Lemma freeable_sz_full n l : freeable_sz n n l ⊣⊢ †{1}l…n ∨ ⌜Z.of_nat n = 0⌝.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index d61c770b6778dc271f07dbbbb73e0568662e70ad..a8c4d60bf69d88afe64915395f00dbb15b5107dc 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
 Section case.
   Context `{!typeG Σ}.
 
-  (* FIXME : have a iris version of Forall2. *)
+  (* FIXME : have an Iris version of Forall2. *)
   Lemma type_case_own' E L C T p n tyl el :
     Forall2 (λ ty e,
       (⊢ typed_body E L C ((p +ₗ #0 ◁ own_ptr n (uninit 1)) :: (p +ₗ #1 ◁ own_ptr n ty) ::