1.1 --- a/doc-src/isac/chuber/bakk_thesis_prelim.tex	Wed Jul 20 09:33:20 2011 +0200
     1.2 +++ b/doc-src/isac/chuber/bakk_thesis_prelim.tex	Wed Jul 20 11:47:32 2011 +0200
     1.3 @@ -23,16 +23,62 @@
     1.4  
     1.5  \section{Background}
     1.6  
     1.7 +``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.
     1.8 +
     1.9 +Presently FP gains importance in face of the ``multi-core crisis'' \cite{}: functional programs are ready to exploit many cores in parallel.
    1.10 +
    1.11 +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.
    1.12 +
    1.13 +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.
    1.14 +
    1.15  \section{Goal}
    1.16  
    1.17 +The goal of this thesis is generation of interactive course material on the topic, implemented in Isabelle and \sisac.
    1.18 +
    1.19 +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.
    1.20 +
    1.21 +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.
    1.22 +
    1.23 +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).
    1.24 +
    1.25  \section{State of the Art}
    1.26  
    1.27 +TODO
    1.28 +
    1.29 +%supports different kinds of function definitions (providing more or less automated support by the prover), mutual, nested and higher-order recursion, partiality
    1.30 +
    1.31 +%Coq \cite{}
    1.32 +
    1.33 +
    1.34  \section{Thesis Structure}
    1.35  
    1.36 +The main point of this thesis is the interactive course material, and the thesis serves this point in several ways:
    1.37 +
    1.38 +general survey on FP
    1.39 +
    1.40 +description of the state of the art in proof tools specialized on FP
    1.41 +
    1.42 +didactic consideration about the course (what has been omitted, ...)
    1.43 +
    1.44 +future work, probably extending the course to more advanced topics
    1.45 +
    1.46 +future work, extending the course to more elementary topics, probably usable at high school
    1.47 +
    1.48 +...
    1.49 +
    1.50 +... 
    1.51 +
    1.52 +
    1.53  \section{Timeline}
    1.54  
    1.55 -%Milestones
    1.56 -%\subsection{TODO}
    1.57 +The main work shall be done during this summer as much as possible.
    1.58 +
    1.59 +Milestones
    1.60 +\subsection{TODO}
    1.61 +study introductory material for Isabelle; contact Alexander Kraus and others for similar course material
    1.62 +
    1.63 +\subsection{TODO}
    1.64 +\sisac =''=
    1.65  
    1.66  %\bibliography{bib/TODO}
    1.67  \end{document}