The existing research is extended to include logical-operational characterizations of computational complexity, i.e., applicative calculi and proof formalisms. Various applications in computing theory and programming methodology also is explored. The PI introduced a new approach to proof theoretic study of computational complexity, which was applied to feasible complexity classes. That approach is exo-algebraic, i.e., referring to free algebras within broader structures. While earlier work used second-order logic to explicitly define free algebras, recent work shows that the exo-algebraic approach can be easily applied also to first-order theories. That approach has the advantages of being free of any initial functions, of permitting foundational delineations of complexity classes, of allowing explicit reference to all computable functions without extending the logic to partially-defined terms, and of having particularly streamlined proof theory and model theory. This work (1) applies exo-algebraic formalisms as above to obtain logic-based, machine-independent classifications of computational complexity classes, thereby relating computational complexity to fundamental parameters of logical complexity; (2) uses these characterizations to obtain new relations between computational complexity and foundations of programming, program verification, type theory, and computational mathematics; and (3) applies the logic-based characterizations to investigate computation complexity proper.
