Institute of Computer Languages
Compilers and Languages Group
über
| Datum: | Mittwoch, 2. Juni 2010 |
|---|---|
| Zeit: | 15:00 c.t. |
| Ort: | TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte) |
ISAC is a "transparent system for applied mathematics" [1], a tutoring- and authoring-system based on the theorem prover Isabelle [2].
After an extensive design phase, supervised by Bruno Buchberger (RISC Linz) and Peter Lucas (TU Graz) in the nineties, in 1999/2000 a mathematics-engine was implemented in SML, rigorously exploiting components of Isabelle. Since then a Java front-end has been developed in cooperation with IICM [3] and field tests demonstrate usability in educational practice [4,5].
ISAC's idea to generate tutoring from an interpretation of programs in "debug mode" is gaining interest by partners on the way to international cooperations [6,7]. Since Peter Lucas has retired, we search for expertise in compiler construction.
The mathematics-engine's programming language is a subset of Isabelle/HOL, the interpreter is written in SML. The status of both, the language and the interpreter, is experimental, has known deficiencies and shall be re-engineered. This re-engineering is the main objective and the main part of the talk.
Furthermore, the question is briefly raised, whether the language (together with some features for proving) can be pushed down from Isabelle to SML. If this push down would be feasible, we would get a powerful language for applied mathematics (overtaking languages like the one of Mathematica), which could be used for both: for production (in standard interpretation) and for tutoring (in the single-stepping interpretation mentioned).
[1] http://www.ist.tugraz.at/projects/isac/
[2] http://isabelle.in.tum.de/index.html
[3] http://www.iicm.tu-graz.ac.at/
[4] http://imst.uni-klu.ac.at/imst-wiki/index.php/Begreifen_und_Mechanisieren_beim_Algebra-Einstieg
[5] http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie
[6] http://www.ist.tugraz.at/projects/isac/publ/plmms-100412.pdf
[7] http://www.ciem.unican.es/proving2010
Walther Neuper is one of the pioneers in introducing computers to
Austrian high-schools in the seventies of the past century. Since then
he has been involved in curriculum development and teacher
education. At Graz University of Technology he investigates
exploitation of CTP technology for educational use.
(http://www.ist.tugraz.at/neuper/)
Sie möchten auf diesen Vortrag durch Aushang hinweisen? Eine druckfertige Einladung im pdf-Format dafür finden Sie hier.