ABSTRACT
One of the major reasons type theory has enjoyed such wide successes is that it is a natural high-level language for computational mathematics and programming, a point that Sol Feferman has effectively made over the years [20, 22]. However, this advantage can sometimes pose a problem because the needs of mathematics and programming can diverge. In mathematics, equality is extensional, where only an object’s value is significant. That is, if the result of f {a ) is b then f { a ) — b, and functions / and g are equal (in A —» B, the space of functions from A to B) exactly when f ( a ) = g{a) for every a in A. In contrast, in the analysis of programs, it is often critical to consider programs intensionally; reasoning about their structure as well as their result value. For example, showing partial correctness of recursive procedures requires reasoning inductively about
the computation of recursive calls. Also, computational complexity certainly depends on a program’s algorithm, and not only on its result.
