An adequate theory of partial computable functions should provide a basis for
defining computational complexity measures and should justify the principle of
computational induction for reasoning about programs on the basis of their
recursive calls. There is no practical account of these notions in type theory,
and consequently such concepts are not available in applications of type theory
where they are greatly needed. It is also not clear how to provide a practical
and adequate account in programming logics based on set theory.
This paper provides a practical theory supporting all these concepts in the
setting of constructive type theories. We first introduce an extensional theory
of partial computable functions in type theory. We then add support for
intensional reasoning about programs by explicitly reflecting the essential
properties of the underlying computation system. We use the resulting
intensional reasoning tools to justify computational induction and to define
computational complexity classes. Complexity classes take the form of
complexity-constrained function types. These function types are also used in
conjunction with the propositions-as-types principle to define a
resource-bounded logic in which proofs of existence can guarantee feasibility of
construction.