Index: /src/ASM/CPP2011/cpp2011.tex
===================================================================
 /src/ASM/CPP2011/cpp2011.tex (revision 1022)
+++ /src/ASM/CPP2011/cpp2011.tex (revision 1023)
@@ 135,4 +135,5 @@
However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset.
To translate a jump to a label, a single conditional jump pseudoinstruction may be translated into a block of three real instructions as follows (here, \texttt{JZ} is `jump if accumulator is zero'):
+{\small{
\begin{displaymath}
\begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l}
@@ 143,5 +144,5 @@
& & & & \mathtt{MOV} & \mathtt{A}\;\;\mathtt{B}
\end{array}
\end{displaymath}
+\end{displaymath}}}
In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
Naturally, if \texttt{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local.
@@ 158,4 +159,5 @@
Yet one more question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?
To understand, again, why this problem is not trivial, consider the following snippet of assembly code:
+{\small{
\begin{displaymath}
\begin{array}{r@{\qquad}r@{\quad}l@{\;\;}l@{\qquad}l}
@@ 166,5 +168,5 @@
\text{5:} & \mathtt{(0x100)} & \texttt{LJMP} & \texttt{0x100} & \text{\texttt{;; Jump backward 256.}} \\
\end{array}
\end{displaymath}
+\end{displaymath}}}
We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8bit byte (0255).
@@ 191,6 +193,5 @@
In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness.
The rest of this paper is a detailed description of our proof that is partly
still in progress.
+The rest of this paper is a detailed description of our proof that is, in part, still a work in progress.
%  %
@@ 209,26 +210,18 @@
\label{sect.matita}
Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent
types that we heavily exploit in the formalization. The syntax of the
statements and definitions in the paper should be selfexplanatory, at least
to those exposed to dependent type theory. We only remark the use of
of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or
sequences of terms to be inferred automatically by the system, respectively.
+Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
+In particular, it features dependent types that we heavily exploit in the formalisation.
+The syntax of the statements and definitions in the paper should be selfexplanatory, at least to those exposed to dependent type theory.
+We only remark the use of of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or sequences of terms to be inferred automatically by the system, respectively.
Those that are not inferred are left to the user as proof obligations.
Pairs are denoted with angular brackets.

Matita features a liberal system of coercions. In particular, it is possible
to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$. The coercion opens a proof
obligation that asks the user to prove that $P$ holds for $x$. When a coercion
must be applied to a complex term (a lambdaabstraction, a local definition,
a case analysis), the system automatically propagates the coercion to the
subterms. For instance, to apply a coercion to force $\lambda x.M : A \to B$
to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from
$M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is
significant when the coercion opens a proof obligation, since the user
will be presented with multiple, but simpler proof obligations in the right
context. Matita supports in this way the proof methodology developed by
Sozeau in~\cite{russell}, but with an implementation that is lighter than the
one of Coq and more integrated in the system.
+Pairs are denoted with angular brackets, $\langle, \rangle$.
+
+Matita features a liberal system of coercions.
+It is possible to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$.
+The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
+When a coercion must be applied to a complex term (a $\lambda$abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the subterms
+ For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$.
+This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
+In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated than that of Coq.
%  %