Certified Cost Bounds in Agda: A Step Towards Automated Complexity Analysis

Automatically computing the time complexity of a recursive program relies on not only extracting recurrence relations from source code, but also proving that the costs obtained by the recurrences are upper bounds on the running time of the code. We do this by proving a bounding theorem, which states that the costs produced by the translation of source programs represent upper bounds on the costs specified by the source language operational semantics. This approach is inspired by the work of Danner, Paykin, and Royer. We formalize our work in Agda, a dependently-typed functional programming language and proof assistant, to ensure that we develop a reliable and mathematically correct system with which to extract recurrences.