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

diff --git a/Chapters/Future.tex b/Chapters/Future.tex
index 3b9161f..852d14f 100644
--- a/Chapters/Future.tex
+++ b/Chapters/Future.tex
@@ -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: