\section{Introduction}
\label{sec:intro}
Compilers and interpreters are among the most complex pieces of software
written to date. Due to the rapid technological development of the last
decades, programming languages have become increasingly complex, semantically
speaking. It has become impossible for a programmer to keep in mind the impact
of their changes on the generated machine code. This led to the
\emph{assumption problem}: developers constantly rely on assumptions about how
the language that they write in works. Intuitive semantics may change over
time, however, and proper definitions are required now that our world relies so
principally on software.

Nowadays, programming languages have semantical specifications as the main link
between programmers and compiler designers. This solves the assumption problem
on the programmer's side. However, now that programming languages become
increasingly complex, the same problem occurs on the compiler designer's side:
the specification has become too complex to efficiently translate it into
imperative code, and writing a correct compiler or interpreter has become no
trivial task.

Functional programming languages offer writers of code processing systems tools
to efficiently work with semantical specifications. Using a high level of
abstraction, the gap between specification and implementation is closed,
allowing for quicker correctness checks and better maintainable code. The
connections between functional languages and mathematics let us \emph{prove}
properties about code processing systems (for example, their correctness with
respect to a specification).

\input{intro-org}
\input{intro-while}