In this project, we employ and set up conceptual frameworks, in particular, theories relating classical mathematics with constructive mathematics and feasible mathematics. Thereby we always emphasize the computational properties and complexities of our formalisms. We use proof theory as our main tool for analyzing the constructive and computational content of various formalisms and aim at further exploiting the proofs as computations paradigm. Besides the traditional subsystems of first- and second-order arithmetic and (admissible) set theory, we will focus on theories of explicit mathematics, operational set theories, and theories of partial truth.