Changeset 1023 for src/ASM/CPP2011

Timestamp:

Jun 21, 2011, 12:23:31 PM (10 years ago)

Author:

mulligan

Message:

changes to english in matita section, shrunk diagrams in introduction to save space

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (6 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -135 +135 @@
 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 +144 @@
        &              &                            &                 & \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 +159 @@
 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 +168 @@
 \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 8-bit byte (0--255).
 
@@ -191 +193 @@
 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 +210 @@
 \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 self-explanatory, 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 self-explanatory, 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 lambda-abstraction, a local definition,
-a case analysis), the system automatically propagates the coercion to the
-sub-terms. 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 sub-terms
+ 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.
 
 % ---------------------------------------------------------------------------- %