Computer-Checked Recurrence Extraction for Functional Programs

Document
Document

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.

    Item Description
    Name(s)
    Thesis advisor: Licata, Daniel R.
    Date
    May 01, 2016
    Extent
    58 pages
    Language
    eng
    Genre
    Physical Form
    electronic
    Discipline
    Rights and Use
    In Copyright - Non-Commercial Use Permitted
    Digital Collection
    PID
    ir:2462