Corrections mineures

dm.tex

@@ -302,13 +302,13 @@ $\mathcal{N}|[n|] \in \mathbb{N}$ so we have $\mathcal{A}|[e|] \in \mathbb{N}$ w
 \item $e = x$.
 \item $e = e_1 o e_2, T = int$.
 \item $e = e_1.f$.
-\item $e = e_1[f \mapto e_2]$.
+\item $e = e_1[f \mapsto e_2]$.
 \item $e = \{f_1 = e_1; \dots; f_n = e_n\}$.
 
 \end{itemize}
 \end{proof}
 
-\begin{lemma}[Well programs cannot go wrong]
+\begin{lemma}[Well typed programs cannot go wrong]
 \[\forall \Gamma P,\quad \Gamma \vdash P \; => \;\forall \sigma,\; (P, \sigma) \not\reduce \bot\]
 \end{lemma}
 
@@ -320,9 +320,7 @@ By induction on the path of $\reduce$, and by induction on the structure/type of
 
 We propose a constraint based static analysis to determine at each instruction which field is defined in each variables.
 Our static analysis is incarnated by the function $RF$ (\enquote{Reachable Fields}).
-
 \[RF : Lab -> Var -> \mathcal{P}(Field)\]
-
 where $Lab$ is the set of labels.
 One unique label is assigned to each instruction.
 For the sake of simplicity, we note $[I]^l$ the instruction of label $l$.