Automatic Definition of Running Time Functions

Chair for Logic and Verification

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]