Certified Cost Bounds in Agda: A Step Towards Automated Complexity Analysis
Document
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.
Item Description
Name(s)
Author: Hudson, Bowornmet
Thesis advisor: Licata, Dan
Date
April 15, 2015
Extent
47 pages
Language
eng
Genre
Physical Form
electronic
Discipline
Rights and Use
In Copyright – Non-Commercial Use Permitted
Digital Collection
PID
ir:711