Remove todo.

[matthijs/master-project/report.git] / Chapters / Future.tex

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index 3b9161f0e61187221e8950a4dc65bb3efda01f54..9c60dfe8e3b8f656ef0bd8a74e67fa6a98b4e80b 100644 (file)
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -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
 
 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
 
 \section{Multiple cycle descriptions}
 In the current Cλash prototype, every description is a single-cycle


@@ -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.
   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: