Permalink
Browse files

Finalize report.

  • Loading branch information...
1 parent d936530 commit 4f0c8ccc7a741db0c418fa91a73bfe3ebaa2fead @jlouis committed May 29, 2009
Showing with 3 additions and 3 deletions.
  1. +1 −1 Makefile
  2. +1 −1 report/intro.tex
  3. +1 −1 report/janus0.tex
View
@@ -1,4 +1,4 @@
-ARCH_TARGET=pre-final
+ARCH_TARGET=final
MODULES := BaseLib Memory Word32 ZStore W32Store Janus0 Janus1
VS := $(MODULES:%=%.v)
View
@@ -12,7 +12,7 @@ \chapter{Introduction}
machine-verifiable form. We thus construct a bridge between
reversibility research and mechanical theorem proving.
-The JANUS programming language were conceived as a student project in
+The JANUS programming language was conceived as a student project in
1982 at Caltech by Chris Lutz and Howard Derby. It was first later
however, with the work in \cite{yokoyama.gluck:reversible,
yokoyama.axelsen.ea:principles} that the language was given a modern
View
@@ -189,7 +189,7 @@ \subsection{Properties of stores}
\begin{multline*}
\forall \sigma, \sigma' \in \Sigma, x \in Loc, v_1, v_2 \in Value
\colon \\
- \sigma[x \mapsto v_1](x) = \sigma[x \mapsto v_2](x) \implies v_1 = v_2
+ \sigma[x \mapsto v_1](x) = \sigma[x \mapsto v_2](x) => v_1 = v_2
\end{multline*}
\end{lem}
\begin{proof}

0 comments on commit 4f0c8cc

Please sign in to comment.