21 TODO |
21 TODO |
22 } |
22 } |
23 |
23 |
24 \section{Background} |
24 \section{Background} |
25 |
25 |
|
26 ``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. |
|
27 |
|
28 Presently FP gains importance in face of the ``multi-core crisis'' \cite{}: functional programs are ready to exploit many cores in parallel. |
|
29 |
|
30 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. |
|
31 |
|
32 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. |
|
33 |
26 \section{Goal} |
34 \section{Goal} |
|
35 |
|
36 The goal of this thesis is generation of interactive course material on the topic, implemented in Isabelle and \sisac. |
|
37 |
|
38 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. |
|
39 |
|
40 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. |
|
41 |
|
42 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). |
27 |
43 |
28 \section{State of the Art} |
44 \section{State of the Art} |
29 |
45 |
|
46 TODO |
|
47 |
|
48 %supports different kinds of function definitions (providing more or less automated support by the prover), mutual, nested and higher-order recursion, partiality |
|
49 |
|
50 %Coq \cite{} |
|
51 |
|
52 |
30 \section{Thesis Structure} |
53 \section{Thesis Structure} |
|
54 |
|
55 The main point of this thesis is the interactive course material, and the thesis serves this point in several ways: |
|
56 |
|
57 general survey on FP |
|
58 |
|
59 description of the state of the art in proof tools specialized on FP |
|
60 |
|
61 didactic consideration about the course (what has been omitted, ...) |
|
62 |
|
63 future work, probably extending the course to more advanced topics |
|
64 |
|
65 future work, extending the course to more elementary topics, probably usable at high school |
|
66 |
|
67 ... |
|
68 |
|
69 ... |
|
70 |
31 |
71 |
32 \section{Timeline} |
72 \section{Timeline} |
33 |
73 |
34 %Milestones |
74 The main work shall be done during this summer as much as possible. |
35 %\subsection{TODO} |
75 |
|
76 Milestones |
|
77 \subsection{TODO} |
|
78 study introductory material for Isabelle; contact Alexander Kraus and others for similar course material |
|
79 |
|
80 \subsection{TODO} |
|
81 \sisac =''= |
36 |
82 |
37 %\bibliography{bib/TODO} |
83 %\bibliography{bib/TODO} |
38 \end{document} |
84 \end{document} |