AAU Student Projects - visit Aalborg University's student projects portal
A master's thesis from Aalborg University
Book cover


Certifying Time Complexity of Agda Programs Using Complexity Signatures

Translated title

Certificering af Tidskompleksitet af Agda Programmer Ved Brug af Kompleksitetssignaturer

Authors

; ;

Term

4. term

Education

Software, Master

Publication year

2020

Submitted on

Pages

86

Abstract

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.

Keywords

dependent types ; program certification ; Agda ; time complexity ; functional programming

Documents

Download
View record in AAU Student Projects