## Bachelor Thesis

The aim of this project is to automate the definition of *running time* functions, i.e. functions that express the time complexity of another function. The automation should translate the definition of some function `f`

in a simple functional language to an analogous function that computes the number of function calls `f`

makes. The translation schema is fairly simple, but it needs to be implemented inside the proof assistant Isabelle in the functional language Standard ML. Thus it requires both *good* functional programming skills and the willingness to familiarize yourself with a new implementation framework (Isabelle).

Programming language:

Standard ML

Prerequisites:

Good functional programming skills in one of ML, OCaml or Haskell; English

Professor:

Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]