diff --git a/SeparationLogic.v b/SeparationLogic.v
index 5ab9f8a..7895f97 100644
--- a/SeparationLogic.v
+++ b/SeparationLogic.v
@@ -93,7 +93,7 @@ Definition trsys_of (h : heap) {result} (c : cmd result) := {|
 |}.
 
 (* Now let's get into the first distinctive feature of separation logic: an
- * assertion language that takes advantage of *pariality* of heaps.  We give our
+ * assertion language that takes advantage of *partiality* of heaps.  We give our
  * definitions inside a module, which will shortly be used as a parameter to
  * another module (from the book library), to get some free automation for
  * implications between these assertions. *)
diff --git a/SharedMemory.v b/SharedMemory.v
index 018064a..4f38798 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -448,7 +448,7 @@ Qed.
  * shared state identically.  In such a case, we may always pick our favorite
  * thread to step next. *)
 
-(* To make all that formal, we will do some static program analyze to summarize
+(* To make all that formal, we will do some static program analysis to summarize
  * which atomic actions a thread might take. *)
 Record summary := {
   Reads : set nat;