diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index a009324a94ae90656f73bcd5144757020790c1bf..06a9f74959f9bad0bc14ead5414f9418e9a1c152 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -367,7 +367,7 @@ The adequacy statement now reads as follows:
 Notice that the state invariant $S$ used by the weakest precondition is chosen \emph{after} doing a fancy update, which allows it to depend on the names of ghost variables that are picked in that initial fancy update.
 
 \paragraph{Hoare triples.}
-It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs in Coq.
+It turns out that weakest precondition is actually quite convenient to work with, in particular when performing these proofs in Coq.
 Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
 \[
 \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \wand \wpre{\expr}[\mask]{\Ret\val.\propB})}