Publication Date

5-2016

Advisor(s)

Daniel R. Licata

Department

Computer Science

Language

English

Abstract

This thesis continues work towards a computer-checked system for automatic complexity analysis of functional programs. Following [DLR15], we extract cost information from a source language to a monadic metalanguage which we call the complexity language, and give a denotational semantics to the complexity language which interprets types as preorders and terms as monotone maps between preorder structures. Building upon the work presented in [Hud15], we extend the source language with more types, and prove that the complexity language is sound relative to its interpretation. In addition, we observe that the recurrences we obtain using our system resemble recurrences obtained manually. We implement all of our work in Agda, a dependently-typed programming language and proof assistant.

Share

COinS
 

© Copyright is owned by author of this document