\documentclass{article}

 \usepackage{a4}

 \usepackage{times}

 \usepackage{latexsym}

 %\bibliographystyle{alpha}

 \bibliographystyle{abbrv}

 \usepackage{graphicx}

 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

 \title{Tentative Title:\\

   Theory of Functional Programming\\

   Introduced by Isabelle and \isac}

 \author{n.n.\\

 {\tt TODO@xxx.at}}

 \begin{document}

 \maketitle

 \abstract{

 TODO

 }

 \section{Background}

 ``Functional programing'' (FP) is one of the leading paradigms in programming besides ``object oriented programming'' \cite{?} and ``logic / constraint programming'' \cite{}. One advantage of FP are general and elegant approaches to the mathematical theory of programming.

 Presently FP gains importance in face of the ``multi-core crisis'' \cite{}: functional programs are ready to exploit many cores in parallel.

 In spite of this fact, at Graz University of Technology (TUG) FP has vanished during recent years, and it is of actual importance to include FP again in education.

 In order to support such education this thesis will employ advanced tools developed in the intersection between computer science and mathematics: The computer theorem prover Isabelle \cite{} and the educational math assistant \sisac.

 \section{Goal}

 The goal of this thesis is generation of interactive course material on the topic, implemented in Isabelle and \sisac.

 In Isabelle the material shall exploit the recently implemented ``function package'' \cite{}. This package is the most advanced in comparison to other provers and supports all what is needed for programming and proving properties of programs.

 Experience shows, that in early phases of programming (as well as of doing mathematics \cite{?}) proceeding step by step in a program is important for learning. This will be done by implementing selected programs into \sisac.

 The interactive course material shall serve in certain courses at TUG and in the recently established ``entry and orientation phase'' (Studien-Eingangs und -Oreintierungs Phase, STEOP).

 \section{State of the Art}

 TODO

 %supports different kinds of function definitions (providing more or less automated support by the prover), mutual, nested and higher-order recursion, partiality

 %Coq \cite{}

 \section{Thesis Structure}

 The main point of this thesis is the interactive course material, and the thesis serves this point in several ways:

 general survey on FP

 description of the state of the art in proof tools specialized on FP

 didactic consideration about the course (what has been omitted, ...)

 future work, probably extending the course to more advanced topics

 future work, extending the course to more elementary topics, probably usable at high school

 ...

 ... 

 \section{Timeline}

 The main work shall be done during this summer as much as possible.

 Milestones

 \subsection{TODO}

 study introductory material for Isabelle; contact Alexander Kraus and others for similar course material

 \subsection{TODO}

 \sisac =''=

 %\bibliography{bib/TODO}

 \end{document}