Skip to main content
PRL Project

Automated Complexity Analysis

by Ralph Benzinger

Many different formal methods for generating provably correct programs have been proposed. At the same time, reasoning about intensional properties of programs---properties of how the programs computes, rather than what---remains difficult.

In this talk, I will present my recent work on automated complexity analysis of functional programs. This includes the definition of a simple cost model for Nuprl's term language, a methodology for reasoning about the time complexity of Nuprl extracts, possible ways to mechanization, and the introduction of my Automated Complexity Analysis prototype.