Danielsson and others have shown that by annotating functions it becomes possible to perform time complexity analysis in functional languages, however the idea of how little annotation is necessary has not been explored.
This paper describes a small library which enables a method for minimal annotation of functions to certify time complexity with a Timed monad. Using this method we develop a library of matrix functions with certified time complexity and implement the Cocke-Younger-Kasami (CYK) parsing algorithm for context-free-grammars which we certify to have a complexity of O(n⁵) in Agda, a dependently typed programming language.