equal
deleted
inserted
replaced
18 \title{\mJava} |
18 \title{\mJava} |
19 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
19 \author{Gerwin Klein \\ Tobias Nipkow \\ David von Oheimb \\ Cornelia Pusch} |
20 \maketitle |
20 \maketitle |
21 |
21 |
22 \begin{abstract} |
22 \begin{abstract} |
23 This formal development defines \mJava, a small fragment of the |
23 This formal development defines {\mJava}, a small fragment of the |
24 programming language Java (with essentially just classes), together with a |
24 programming language Java (with essentially just classes), together with a |
25 corresponding virtual machine and a specification of its bytecode verifier. |
25 corresponding virtual machine and a specification of its bytecode verifier. |
26 It is shown that \mJava and the given specification of the bytecode |
26 It is shown that {\mJava} and the given specification of the bytecode |
27 verifier are type-safe. |
27 verifier are type-safe. |
28 \end{abstract} |
28 \end{abstract} |
29 |
29 |
30 \tableofcontents |
30 \tableofcontents |
31 \parindent 0pt \parskip 0.5ex |
31 \parindent 0pt \parskip 0.5ex |