My-thesis-to-be
 

• The complexity of type-1 recursive functions had been well studied in the past several decades. On the theoretical side, the study had successfully given a solid ground to the understanding of the structure of the complexity families. On the practical side, the study gives the legitimacy of many criteria, for examples, P vs. NP, or the asymptotic notations such as the big-O notation.
• However, the computational behaviors of higher-ordered functionals are still far beyond understood, theoretically, although the higher-ordered functionals had been widely used in computer science very early on. For example, a programming language that allows functions as arguments is a typical type-2 system. We need a way to characterize those function(al)s in such kind of systems for a long time. The difficulity comes from the lack of a feasible and solid computational model for type-2 or higher functionals.
• We are aiming at the type-2 functionals. We want to give a machine-based model, for example, the Oracle Turing Machine equipped with a clock, to characterize the type-2 functional. Then, we examine the model and attack its limitation alone the line of classical study with many prospects, e.g., Recursion and Sub-recursion Theory, Axiomatic Complexity, Topology, Formal Method, etc..
• Follow the study, we may have several applications. On the theoretical side, we can draw a clearer line of computability in the class of type-2 functionals, and we can formally define the meaning of intuitively feasible functionals. On the practical side, we can give an analogue notion of big-O in type-1 for type-2 functionals, and we can analyze the complexity of theorem proving in a formal system or IIM (Inductive Inference Machine).
• OK! OK!  I am a father of two. It's real.