diff --git a/docs/algebra.tex b/docs/algebra.tex
index 5c2222caa82eb72514ba1345153184a975cc83ab..dc8bdead2a4ecf03b35cda890b1889420fca2241 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -1,4 +1,4 @@
-\section{Algebraic structures}
+\section{Algebraic Structures}
 
 \subsection{OFE}
 
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 63e44070dd919baf13c3dd12ca3047524dc25bc7..2a45cae7cbd88a1fc94619caf86a6a06aadb95df 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -1,4 +1,4 @@
-\section{Base logic}
+\section{Base Logic}
 \label{sec:base-logic}
 
 The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 1ec372c848fdea1b7c94d6fbab730365c2e4e5f4..0a205d8450d472dd288c9f6e4f9ddde69b5c071a 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -17,7 +17,7 @@ Note that in the definition of the carrier $\latert\cofe$, $\latertinj$ is a con
 $\latert(-)$ is a locally \emph{contractive} functor from $\OFEs$ to $\OFEs$.
 
 
-\subsection{Uniform predicates}
+\subsection{Uniform Predicates}
 
 Given a CMRA $\monoid$, we define the COFE $\UPred(\monoid)$ of \emph{uniform predicates} over $\monoid$ as follows:
 \begin{align*}
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index 4dc9f16269e0d0a9da35ab162e74594de2b02a7b..bd10d54efa60000c9290d79789776440300a521a 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -1,4 +1,4 @@
-\section{Extensions of the base logic}
+\section{Extensions of the Base Logic}
 
 In this section we discuss some additional constructions that we define within and on top of the base logic.
 These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 079b811d3e336536ee6ac65d45d008f19a600da8..06a9f74959f9bad0bc14ead5414f9418e9a1c152 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -5,7 +5,7 @@
 This section describes how to build a program logic for an arbitrary language (\cf \Sref{sec:language}) on top of the base logic.
 So in the following, we assume that some language $\Lang$ was fixed.
 
-\subsection{Dynamic composeable higher-order resources}
+\subsection{Dynamic Composeable Higher-Order Resources}
 \label{sec:composeable-resources}
 
 The base logic described in \Sref{sec:base-logic} works over an arbitrary CMRA $\monoid$ defining the structure of the resources.
@@ -101,7 +101,7 @@ We will typically leave the $M_i$ implicit when asserting ghost ownership, as th
 
 
 
-\subsection{World satisfaction, invariants, fancy updates}
+\subsection{World Satisfaction, Invariants, Fancy Updates}
 \label{sec:invariants}
 
 To introduce invariants into our logic, we will define weakest precondition to explicitly thread through the proof that all the invariants are maintained throughout program execution.
@@ -137,7 +137,7 @@ The following assertion states that an invariant with name $\iname$ exists and m
 \[ \knowInv\iname\prop \eqdef \ownGhost{\gname_{\textmon{Inv}}}
   {\authfrag \mapsingleton \iname {\aginj(\latertinj(\wIso(\prop)))}} \]
 
-\paragraph{Fancy updates and view shifts.}
+\paragraph{Fancy Updates and View Shifts.}
 Next, we define \emph{fancy updates}, which are essentially the same as the basic updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
 \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
 Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
@@ -244,7 +244,7 @@ Still, just to give an idea of what view shifts ``are'', here are some proof rul
   {\FALSE \vs[\mask_1][\mask_2] \prop }
 \end{mathparpagebreakable}
 
-\subsection{Weakest preconditions}
+\subsection{Weakest Precondition}
 
 Finally, we can define the core piece of the program logic, the assertion that reasons about program behavior: Weakest precondition, from which Hoare triples will be derived.
 
@@ -439,7 +439,7 @@ We only give some of the proof rules for Hoare triples here, since we usually do
 %   {\knowInv\iname\propC \proves \hoare{\prop}{\expr}{\Ret\val.\propB}[\mask \uplus \set\iname]}
 \end{mathparpagebreakable}
 
-\subsection{Invariant namespaces}
+\subsection{Invariant Namespaces}
 \label{sec:namespaces}
 
 In \Sref{sec:invariants}, we defined an assertion $\knowInv\iname\prop$ expressing knowledge (\ie the assertion is persistent) that $\prop$ is maintained as invariant with name $\iname$.