A type-theory for higher-order amortized analysis

Verification of worst-case bounds (on the resource usage of programs) is an important problem in computer science. The usefulness of such verification depends on the precision of the underlying analysis. For precision, sometimes it is useful to consider the average cost over a sequence of operations, instead of separately considering the cost of each individual operation. This kind of an analysis is often referred to as amortized resource analysis. Typically, programs that optimize their internal state to reduce the cost of future executions benefit from such approaches. Analyzing resource usage of a standard functional (FIFO) queue implemented using two functional (LIFO) lists is a classic example of amortized analysis. In this thesis we present λamor, a type-theory for amortized resource analysis of higher-order functional programs. A typical amortized analysis works by storing a ghost state called the potential with data structures. The key idea underlying amortized analysis is to show that, the available potential with the program is sufficient to account for the resource usage of that program. Verification in λamor is based on internalizing this idea into a type theory. We achieve this by providing a general type-theoretic construct to represent potential at the level of types and then building an affine type-theory around it. With λamor we show that, type-theoretic amortized analysis can be performed using well understood concepts from sub-structural and modal type theories. Yet, it yields an extremely expressive framework which can be used for resource analysis of higher-order programs, both in a strict and lazy setting. We show embeddings of two very different styles (one based on effects and the other on coeffects) of type-theoretic resource analysis frameworks into λamor. We show that λamor is sound (using a logical relations model) and complete for cost analysis of PCF programs (using one of the embeddings). Next, we apply ideas from λamor to develop another type theory (called λcg) for a very different domain – Information Flow Control (IFC). λcg uses a similar typetheoretic construct (which λamor uses for the potential) to represent confidentiality label (the ghost state for IFC). Finally, we abstract away from the specific ghost states (potential and confidentiality label) and describe how to develop a type-theory for a general ghost state with a monoidal structure.