Permalink
Browse files

Ispell document.

  • Loading branch information...
1 parent b58ae48 commit 1d840c72c9f974a8704c19861f18a831798847d0 @jlouis committed May 26, 2009
Showing with 5 additions and 6 deletions.
  1. +1 −1 report/fulljanus.tex
  2. +2 −2 report/intro.tex
  3. +1 −1 report/janus0.tex
  4. +1 −1 report/janus1.tex
  5. +0 −1 report/master.tex
View
@@ -137,7 +137,7 @@ \section{Properties of full JANUS}
the discrimination utterly fails.
This development was unexpected. We initially thought the proof to
-hold and we targetted minor fixes to the semantics to make it
+hold and we targeted minor fixes to the semantics to make it
machine-verifiable. But now we know that it is not simple to carry out
the proof of backwards determinism with the given loop-semantics. In
the paper \cite{yokoyama.axelsen.ea:principles} it is stated that the
View
@@ -25,7 +25,7 @@ \chapter{Introduction}
Our motivation for formalizing JANUS inside the machine is that of
reassurance and knowledge. We will be assured that the language has a
working formalization and that key theorems are true. A mechanical
-correctness check by a machine is much less amenable to oversigts or a
+correctness check by a machine is much less amenable to oversights or a
wrong proof. In fact, if you trust the computation kernel in the
theorem prover of choice, no logical error is possible.
@@ -38,7 +38,7 @@ \chapter{Introduction}
had before. Formality enforces us to optimize and make precise the
definitions and results, which in turn sharpens and refines our
knowledge of a field. A better understanding through formality makes
-it easier to gather new knowlegde in a field.
+it easier to gather new knowledge in a field.
Finally, the meta-theoretic properties of reversible languages are
rather unique to the field. Hence, the community of mechanical
View
@@ -559,7 +559,7 @@ \subsection{Proving determinism of \janusz{}}
language must be deterministic in the forward direction, so there is
only one possible outcome of any computation. Also, it must be
deterministic in the backwards direction: If 2 evaluations of the
-same statement results in the same store-configuration, the inital
+same statement results in the same store-configuration, the initial
configuration must have been equivalent.
We now formally define and prove forwards determinism.
View
@@ -70,7 +70,7 @@ \section{32-bit Integers}
is turn makes them rather bad candidates as a number base. Perhaps
except for the base $2^n$ which can be defined as polynomials of
bits. In any case, Galois-fields are not easily
- machine-implementible in hardware, so we choose not the pursue this
+ machine-implementable in hardware, so we choose not the pursue this
idea further.
\end{rem}
View
@@ -60,7 +60,6 @@
\pagebreak
\tableofcontents
\pagebreak
-\fixme{Ispell from here once everything is finished}
\input{intro}
\input{cocext}
\input{janus0}

0 comments on commit 1d840c7

Please sign in to comment.