fix typos pointed out reviewers

compcertoe/compcertoe.tex

@@ -838,10 +838,10 @@ \subsection{Overview} %{{{
 alongside matching edges:
 \begin{itemize}
 \item Layered composition ($\odot$) acts horizontally.
-  It connects strategies at a common endpoint (\emph{ie.}~effect signature)
+  It connects strategies at a common endpoint (\emph{i.e.}~effect signature)
   over which they are made to interact,
   and connects refinement squares alongside a common
-  vertical edge (\emph{ie.}~refinement convention),
+  vertical edge (\emph{i.e.}~refinement convention),
   which ensures that the refinement properties
   are based on compatible abstractions and constraints.
   %assumptions of one refinement proof
@@ -1006,7 +1006,7 @@ \subsection{Effect Signatures} \label{sec:esig} %{{{
 $\vec{v} \in \kw{val}^*$ are the actual parameters, and
 $m \in \kw{mem}$ is the memory state at the time of invocation;
 answers take the form $v'@m'$ where
-$v' \in \kw{val}$ is value returned by the function~$f$ and
+$v' \in \kw{val}$ is the value returned by the function~$f$ and
 $m' \in \kw{mem}$ is the new state of the memory.
 This is captured by the effect signature
 \[
@@ -1975,7 +1975,7 @@ \subsection{Strategies} \label{sec:model:strat} %{{{
 Unlike $\sigma_{\vec{q}}$ above,
 many strategies of interest are stateless
 in the sense that every incoming question
-is handled in that same way
+is handled in the same way
 regardless of any previous history.
 %Following \citet{objsem},
 %we call such strategies \emph{regular}.
@@ -2400,7 +2400,7 @@ \subsection{Refinement Conventions} %{{{
     \emph{all possible pairs of answers} $(n_1, n_2)$
     are permitted by $\mathbf{R}^\bullet_{m_1m_2}$.
     However, no questions are allowed beyond that point
-    until pays of the following kind are added to the refinement convention.
+    until plays of the following kind are added to the refinement convention.
   \item The play $(m_1, m_2)(n_1,n_2) s$
     extends the ``next'' convention $\mathbf{R}^{n_1,n_2}_{m_1,m_2}$
     with the play $s$.
@@ -2514,7 +2514,7 @@ \subsection{Refinement Squares} %{{{
 we recursively define a family of relations
 $\unlhd^x_{\mathbf{R} \twoheadrightarrow \mathbf{S}}$
 between the possible plays of $\sigma$
-and the possible rediduals of $\tau$.
+and the possible residuals of $\tau$.
 Using the short-hands 
 $\mathbf{R}' := (m_1,m_2)(n_1,n_2) \backslash \mathbf{R}$ and
 $\mathbf{S}' := (q_1,q_2)(r_1,r_2) \backslash \mathbf{S}$,
@@ -3483,7 +3483,7 @@ \section{Compositional State} \label{sec:scomp} %{{{
 which serves as a foundation of our compositional treatment of state.
 We omit many formal definitions
 in the interest of space and readability,
-but they can be found in the Appendix~A.
+but they can be found in Appendix~A.
 
 %}}}
 
@@ -3687,7 +3687,7 @@ \subsection{Explicit State} %{{{
     %The types are explained in \S\ref{sec:overview}.
     The overall specification $\Gamma_\kw{bq}$
     describes the queue operations in terms of
-    a sequence values $\vec{q} \in D_\kw{bq} := V^*$.
+    a sequence of values $\vec{q} \in D_\kw{bq} := V^*$.
     Verification can be decomposed using the intermediate specifications
     $\Sigma_\kw{bq}$ and $\Gamma_\kw{rb}$ for
     $\kw{bq.c}$ and $\kw{rb.c}$.}
@@ -5322,7 +5322,7 @@ \subsection{Memory Separation}
 whose values must match the high-level abstract state
 and will be updated according to the specification.
 Also,
-The initial memory share $m_0 := \kw{init\_mem}(\kw{rb.c})$
+the initial memory share $m_0 := \kw{init\_mem}(\kw{rb.c})$
 associated with $\kw{rb.c}$ satisfies
 $\zeta_\kw{rb} : d_0 \mathrel{R_\kw{rb}} m_0$.
 The remaining part of the memory should not be changed by $\kw{rb.c}$.
@@ -5361,8 +5361,8 @@ \subsection{Memory Separation}
 which contains only the variables $\kw{buf}$, $\kw{c1}$ and $\kw{c2}$.
 
 On one end,
-the program must mange
-all the memory shared passed
+the program must manage
+all the memory shares passed
 from the client.
 To achieve this,
 we can use the Clight frame property for $\kw{rb.c}$
@@ -5491,7 +5491,7 @@ \subsection{Modeling loading and the execution environments}
 
 Verifying functionailities
 of library code substantially benefits from
-the CompCertO's open semantics.
+CompCertO's open semantics.
 However,
 the openness hinders reasoning
 on the behavior of executables.
@@ -5532,9 +5532,9 @@ \subsection{Modeling loading and the execution environments}
 The return address $\kw{RA}$
 and the stack pointer $\kw{RSP}$
 are initialized to $\kw{null}$
-according to the CompCertO's simulation convention.
+according to CompCertO's simulation convention.
 At the end,
-the value stored in the $\kw{RAX}$ is returned.
+the value stored in $\kw{RAX}$ is returned.
 
 On the other end,
 the $\kw{runtime} : \mathcal{S} \rightarrow \mathcal{A}$
@@ -5598,14 +5598,14 @@ \subsection{Modeling loading and the execution environments}
 
 \paragraph{Verifying Loaded Programs}
 
-Reasoning the process behavior
+Reasoning about the process behavior
 directly at the level of assembly programs
 is intricate because of
 the large abstraction gap between
 the strategy-level specifications
 and the assembly semantics.
 Therefore,
-We also introduce a loader
+we also introduce a loader
 for the $\kw{Clight}$ semantics
 to divide the proof
 into manageable pieces.
@@ -5682,7 +5682,7 @@ \subsection{Modeling loading and the execution environments}
   \,.
 \end{align*}
 Note the $\oplus$ operator here
-is the CompCertO's linking operator,
+is CompCertO's linking operator,
 which should not be confused
 with the flat composition
 on strategies.
@@ -6345,7 +6345,7 @@ \section{Related and Future Work} \label{sec:rw} %{{{
 
 \paragraph{Multi-language Semantics} %{{{
 
-We have demonstrated that our framework is able to reason across languauges through non-trivial examples such as the one in Fig~\ref{fig:readwritehello}.
+We have demonstrated that our framework is able to reason across languages through non-trivial examples such as the one in Fig~\ref{fig:readwritehello}.
 In Compositional CompCert and CompCertM,
 assembly programs are given C-level semantics,
 making it possible to directly reason about composite programs
@@ -6405,7 +6405,7 @@ \section{Related and Future Work} \label{sec:rw} %{{{
 In contrast,
 our strategy model
 adheres to a transitional approach
-where plays consist solely events.
+where plays consist of solely events.
 Here, dual nondeterminism
 is concealed within the construction of
 refinement conventions and simulations,