It is notoriously hard to express computational complexity properties of programs in programming logics based on a semantics which respects extensional function equality. This is a serious impediment to certain key applications of programming logics, even those which apply very well otherwise.
This paper shows how to define computational complexity measures in such logics as long as they support inductively defined types, dependent products, and functions. The method exploits a natural feature of inductive definitions in type theory, namely that implicit codes are kept with the objects showing how they are presented in the inductive class.
The adequacy of the proposed definition depends on a faithfulness
theorem showing that the external (or meta-level) definition of
complexity is respected by the internal definition. The results are
applied to defining resource bounded quantifiers that can be used to
state complexity constraints on constructive proofs and their
extracted programs. In such resource bounded logic it is
possible to prove theorems like a PTime axiom of choice. The results
of the paper bridge the fields of semantics and complexity to a