\section{Introduction}
\label{sec:intro}
Compilers and interpreters are very complex pieces of software. 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. Developers now constantly rely on assumptions about how the
language they are using actually 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 problem on the
programmer's side. However, with the increasing complexity of programming
languages, another 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 is no longer a
trivial task.

Functional programming languages offer writers of code processing systems tools
to efficiently work with semantical specifications --- indeed, functional
programs can be used as the very specification themselves~\citep{fpasspec}.
However, we will not go this far. While functional programs are indeed better
suitable for semantic specifications than natural language, mathematical
notation gives even more freedom~\citep[as demonstrated by e.g.][]{proganal}.
We therefore suggest tools for the implementation of these mathematical
definitions in a functional style.

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
allow us to \emph{prove} properties about code processing systems (for example,
their correctness with respect to the specification).

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