Computer-Checked Recurrence Extraction for Functional Programs
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.