Institute of Computer Languages
Compilers and Languages Group

Talks 2010 - Walther Neuper

Der Arbeitsbereich für Programmiersprachen und Übersetzer am Institut für Computersprachen lädt zu folgendem Vortrag ein:

Dr. Walther Neuper

Technische Universität Graz, Österreich

über

Tutoring <-- Single Stepping Interpretation of Functional Programs

Datum: Mittwoch, 2. Juni 2010
Zeit: 15:00 c.t.
Ort: TU Wien, Bibliothek E185.1, Argentinierstraße 8, 4. Stock (Mitte)

Zusammenfassung:

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

Kurzbiographie von Dr. Walther Neuper

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.

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)