\documentclass[12pt]{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 (or constraint) programming'' \cite{?}. One advantage of FP are general and elegant approaches to the mathematical theory of programming \cite{?}.

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 compile a course based on advanced tools developed in the intersection between computer science and mathematics: The computer theorem prover Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and the educational math assistant \sisac.

\section{Goal}

The goal of this thesis is generation of interactive course material on FP and respective theory of programming, implemented in Isabelle and \sisac.

The material shall use most recent developments, for instance the ``function package'' \cite{krauss:funs,krauss:termination07,krauss:partial06} recently implemented in Isabelle. This package supports all what is needed for programming and proving properties of programs.

Although addressing most recent developments and theory at the state of the art, the material also shall serve in early phases of programming. Experience shows, that in early phases (in analogy to 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 -Orientierungs Phase, STEOP).

\section{State of the Art}

The thesis cover a wide range of topics some of which will be presented in more detail to be agreed on.

\paragraph{Theory of functional programming ?}

TODO

\paragraph{Proof tools for FP}

Isabelle's function package \cite{krauss:funs} is the most advanced in comparison to other provers. It supports two different way of function definitions, one providing full automation (applicable in simple cases) and another featuring interactive proofs of termination.

The function package covers the full range of FP:  mutual, nested and higher-order recursion, partiality

The other European computer theorem prover, Coq \cite{}, has less powerful support for FP (TODO)

\paragraph{Didactics of FP} is concern of very different opinions: At some universities FP is addressed in introductory courses, while at other universities FP is considered an abstract topic addressed in higher semesters. The choice between these extreme alternatives seems to be related to principcal considerations on software construction \cite{aichernig:ingenieur}.

The planned course might provide a bridge between the alternatives, addressing novices as well as advanced students by employing computer theorem provers.

\paragraph{Educational math assistants,} if based on computer theorem proving, are appropriate to serve introduction to FP in a specific way: If considering evaluation of functional programs as rewriting, there is an obstacle. Empirical data show that students do not learn to apply rules at high-school --- for instance, the cannot apply the law of distributivity in algebra consciously, they do algebra in the same way they they use their mother language.

The experimental system \sisac{}\footnote{http://www.ist.tugraz.at/projects/isac/} developed at TU Graz seems appropriate to provide experience in rigorous application of rewrite rules as a prerequisite to understand evaluation in FP.

\section{Thesis Structure}

The main result of this thesis is the interactive course material, accompanied by a thesis.

\paragraph{The interactive course material} will be implemented as Isabelle theories. Isabelle provides a document preparation system for theories which shall lead for a twofold presentation of the course: as (a) pdf-file(s) and as theories supporting interactive learning.

For stepwise exercises in \sisac{} an additional Isabelle theory is required, which contains the specifications and programs for the respective exercises in ML-sections.

\paragraph{The thesis} completes the work as required for a bakkalaureate.

%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{references}

\end{document}