Bachelor's Thesis

Various tools in the Isabelle theorem prover produce theorems involving numerical data. Such results are best communicated by visualizing the numerical data points. When proving theorems about functions over the real numbers, the user might find it helpful to request plots of the involved functions, e.g., x -> sin(x) + x * exp(x).

The aim of this thesis is to implement a facility to plot functions and numerical data using Isabelle's document preparation system (implemented in Standard ML), which translates Isabelle theories to LaTeX source.

In addition to the static document preparation, offering plotting capabilites in Isabelle's IDE (implemented in Scala) would be desirable.

Prerequisites:
Functional programming, LaTeX, (Scala)
Supervisor:
Fabian Immler
Professor:
Prof. Tobias Nipkow