Formalising time complexity in Agda

Potential supervisors: 

Once upon a time I implemented a kind of time complexity analysis monad in Agda. [1] By using this monad one can include time complexity information in type signatures. One of my examples was the minimum  function, implemented by first sorting the list using insertion sort, and then returning the sorted list's first element. In a non-strict language this function runs in linear time, and this was also reflected in the function's type signature:
  minimum : Vec A (1 + n) → Thunk (8 + 5 ∗ n) A

Returning the last element is, in the worst case, considerably less efficient. This was reflected in the type signature of the maximum function:
  maximum : Vec A (1 + n) → Thunk (13 + 14 ∗ n + 4 ∗ n ^ 2) A

The goal of this project is to formally verify the time complexity of some algorithms (more complicated than minimum and maximum). The algorithms could perhaps be taken from a text book on algorithms or data structures. One option is to use the time complexity monad mentioned above, but other approaches are also possible. In fact, it might be a good idea to study different approaches before deciding which one to use.

Prerequisites: Students attempting this project should have a good background in algorithm analysis, as well as experience using a proof assistant such as Agda.

[1] "Lightweight Semiformal Time Complexity Analysis for Purely
Functional Data Structures":