\abstract{}

\section{Introduction}

  The department has constructed a generic rewrite framework. This framework is
  very useful, but can be error prone to use.

\section{Expression data type}

  Suppose we are writing an interpreter for a simple logical expression
  language.

\section{Express generic rewrite rules}

  Before interpretation, we might want to express optimizations and
  simplifications as rewrite rules. The rewrite framework allows us to do so.

\section{Using the generic rewrite function}

  The generic rewriteM function allows us to rewrite every value of every data type.
  
\section{Generics by fixpoint view}

  The only thing we have to do is give a structural representation for our data
  type. In this view we make sums, products, constructors and fixpoints
  explicit.

\section{Possible problems}

  Although this framework is very useful and simple to use, things can go wrong
  when used improperly.

  We cannot use the type system to demand the correctness of the rewrite
  function, the soundness and completeness of the representations and the
  semantical soundness of the rules.
  
\section{Our solution}

  To make sure that both implementation and usage of the framework is done
  correctly, we test the properties use QuickCheck.

\section{Rewrite property}

\section{View soundness + example}

\section{Semantic soundness + example}

% ---------------------------------------------------------

\section{Arbitrary instances}
Show the instance of arbitrary for Tree and the corresponding fixpoints.
Show the instance of arbitrary for Direction and the corresponding fixpoints.
\section{Tree fixpoints}
\section{Direction fixpoints}
\section{Our solution: gfixpoints}
\section{Arbitrary instances: generically}
Show and explain the generic version of arbitrary.
\section{Calculating the fixpoints}
Explain how the fixpoint-tree is calculated and how it has the structure as the
sums of products.
\section{Summary}
Give a summary of how everything works together
\section{Conclusion}
Restate what we did and why it is important.