Certifying Time Complexity of Agda Programs Using Complexity Signatures

Student thesis: Master thesis (including HD thesis)

  • Simon Quist Rannes
  • Johannes Elgaard
  • Christian Bach Møllnitz
4. term, Software, Master (Master Programme)
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.
LanguageEnglish
Publication date14 Jun 2020
Number of pages86
ID: 334206514