Hilbert's program aimed to resolve the foundational crisis of mathematics by showing that it is always possible to eliminate the use of infinitary methods from proofs of concrete results of finite mathematics. Gödel showed with his Second Incompleteness Theorem that this goal is not achievable in full generality. Gentzen's famous consistency proof of first order Peano arithmetic has initiated the modern field of ordinal analysis which aims to characterize the concrete consequences of the analyzed abstract theories by computation of characteristic ordinals. A functorial approach to ordinal analysis was initiated by Girard and is currently actively pursued by the research group in UGent and others. The key insight is that there is a close connection between the logical complexity of the language of second order arithmetic and the simple types of higher-order functorial operators on well-orders. This project aims to extend this general approach to the much more advanced level of third order arithmetic (TOA). For this, I will generalize this theory to the case of polymorphic types. On the level of type systems, this corresponds to a jump from simply typed lambda calculus to Girard's System F, adding significant expressive power. The main objective of this proposal is to establish the connection between logical complexity classes and these new objects in the context of TOA. This should open the door to the development of proof theory for systems of TOA.