PRL Seminars

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.