statically estimating the execution cost of a program. However, when
one is interested in how the execution costs of two programs compare
to each other (i.e., relational cost analysis), the use of unary techniques
does not work well in many cases. In order to support a relational cost
analysis, we must ultimately support reasoning about not only the
executions of a single program, but also the executions of two programs,
taking into account their similarities. This dissertation makes several
contributions to the understanding and development of such a relational
cost analysis. It shows how:
1) Refinement types and effect systems can express functional and
relational quantitative properties of pairs of programs, including the
difference in execution costs; 2) Relational cost analysis can be adapted
to reason about dynamic stability, a measure of the update times of incremental
programs as their inputs change; and 3) A sound and complete bidirectional
type system can be developed (and implemented) for relational cost analysis.