X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FFuture.tex;h=4eb297d7e9c3d2b357942bfec82359017a263699;hp=3b9161f0e61187221e8950a4dc65bb3efda01f54;hb=a4cfdaa1ccacc0dcf9a374bb202b247b8f28dccb;hpb=fdfc1c6248fdde5cb20ae08b0fc4268433731d10

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index 3b9161f..4eb297d 100644
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -126,7 +126,7 @@ Note that the \hs{FooState} type has changed (so indirectly the type of
 stateful functions at a time, the final state consists of nested two-tuples.
 The final \hs{()} in the state originates from the fact that the \hs{return}
 function has no real state, but is part of the composition. We could have left
-out the return statement (and the \hs{outb <-} part) to make \hs{foo}'s return
+out the return expression (and the \hs{outb <-} part) to make \hs{foo}'s return
 value equal to \hs{funcb}'s, but this approach makes it clearer what is
 happening.
 
@@ -356,7 +356,7 @@ Note that in the above example the \hs{suba} and \hs{subb} functions are
 is calculated as well, but only saved when the right clock has an up
 transition.
 
-As you can see, there is some code duplication in the case statement that
+As you can see, there is some code duplication in the case expression that
 selects the right clock. One of the advantages of an explicit approach like
 this, is that some of this duplication can be extracted away into helper
 functions. For example, we could imagine a \hs{select_clock} function, which
@@ -391,8 +391,8 @@ behaviour is not needed.
 
 The main cost of this approach will probably be extra complexity in the
 compiler: The paths (state) data can take become very non-trivial, and it
-is probably hard to properly analyze these paths and produce the intended VHDL
-description.
+is probably hard to properly analyze these paths and produce the
+intended \VHDL description.
 
 \section{Multiple cycle descriptions}
 In the current Cλash prototype, every description is a single-cycle
@@ -573,7 +573,7 @@ lightly.
     This is of course a very intrusive solution. Every type must become member
     of this typeclass, and there is now some member in every type that is a
     special don't care value. Guaranteeing the obvious don't care semantics
-    also becomes harder, since every pattern match or case statement must now
+    also becomes harder, since every pattern match or case expressions must now
     also take care of the don't care value (this might actually be an
     advantage, since it forces designers to specify how to handle don't care
     for different operations).
@@ -615,3 +615,13 @@ lightly.
   These options should be explored further to see if they provide feasible
   methods for describing don't care conditions. Possibly there are completely
   other methods which work better.
+
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system.  In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
+% vim: set sw=2 sts=2 expandtab: