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).
Good functional programming skills in one of ML, OCaml or Haskell; English