From 06d2ac31a9a07bd8d73f9f4792abd8dc97c4649e Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 21 Apr 2022 18:45:13 +0100
Subject: Add an index

---
 chapters/background.tex | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'chapters/background.tex')

diff --git a/chapters/background.tex b/chapters/background.tex
index 7208050..19a8c15 100644
--- a/chapters/background.tex
+++ b/chapters/background.tex
@@ -213,15 +213,15 @@ of the compiler, meaning this method of proving algorithms correct ensures a cor
 
 \subsection{CompCert}
 
-CompCert~\cite{leroy09_formal_verif_compil_back_end} is a formally verified C compiler written in
-Coq~\cite{bertot04_inter_theor_provin_progr_devel}.  Coq is a theorem prover, meaning algorithms
-written in Coq can be reasoned about in Coq itself by proving various properties about the
-algorithms.  To then run these algorithms that have been proven correct, they can be extracted
-directly to OCaml code and then executed, as there is a straightforward correspondence between Coq
-and OCaml code.  During this translation, all the proofs are erased, as they are not needed during
-the execution of the compiler, as they are only needed when the correctness of the compiler needs to
-be checked.  With this process, one can have a Compiler that satisfies various correctness
-properties and can therefore be proven to preserve the behaviour of the code.
+\index{CompCert}CompCert~\cite{leroy09_formal_verif_compil_back_end} is a formally verified C
+compiler written in Coq~\cite{bertot04_inter_theor_provin_progr_devel}.  Coq is a theorem prover,
+meaning algorithms written in Coq can be reasoned about in Coq itself by proving various properties
+about the algorithms.  To then run these algorithms that have been proven correct, they can be
+extracted directly to OCaml code and then executed, as there is a straightforward correspondence
+between Coq and OCaml code.  During this translation, all the proofs are erased, as they are not
+needed during the execution of the compiler, as they are only needed when the correctness of the
+compiler needs to be checked.  With this process, one can have a Compiler that satisfies various
+correctness properties and can therefore be proven to preserve the behaviour of the code.
 
 CompCert contains eleven intermediate languages, which are used to gradually translate C code into
 assembly that has the same behaviour.  Proving the translation directly without going through the
@@ -237,13 +237,13 @@ allocation and making sure that the stack variables are correctly aligned.
 
 \subsubsection{CompCertSSA}
 
-CompCertSSA is an extension of CompCert with an additional \SSA\ intermediate language.  This
-language enforces \SSA\ properties and therefore allows for many convenient proofs about
-optimisations performed on this intermediate language, as many assumptions about variables can be
-made when these are encountered.  The main interesting porperty that arises from using \SSA\ is the
-\emph{equational lemma}, stating that given a variable, if it was assigned by an operation that does
-not depend on memory, then loading the destination value of that variable is the same as recomputing
-the value of that variable with the current context.
+\index{CompCertSSA}CompCertSSA is an extension of CompCert with an additional \SSA\ intermediate
+language.  This language enforces \SSA\ properties and therefore allows for many convenient proofs
+about optimisations performed on this intermediate language, as many assumptions about variables can
+be made when these are encountered.  The main interesting porperty that arises from using \SSA\ is
+the \emph{equational lemma}, stating that given a variable, if it was assigned by an operation that
+does not depend on memory, then loading the destination value of that variable is the same as
+recomputing the value of that variable with the current context.
 
 Given a well formed SSA program $p$, a reachable state $\Sigma\ s\ f\ \sigma\ R\ M$, a memory
 independent operation which was defined at a node $d$ as $\mono{Iop}\ \mathit{op}\ \vec{a}\ x\ n$
-- 
cgit 

