In type application Rule :
$$\dfrac{ \Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}} { \Gamma \vdash t_1 \ t_2 : T_{12} } \textsf{ (T-App)}$$
if we deriving the term from bottom up, how to get $T_{11}$ from ? How you'll know what is $T_{11}$? Its not clear to me.
You can look at this rule in two ways:
As a checking rule, it says that, to verify that $t_1 t_2$ has type $T_{12}$, we check that there exists some $T_{11}$ such that $t_1 : T_{11} \to T_{12}$, and we check that $t_2 : T_{11}$. If these checks hold, then the typing of the application must hold.
As an inference rule, it says that to infer the type of $t_1 t_2$, we infer the type of $t_1$ and verify that it has the form $T_{11} \to T_{12}$ for some types $T_{11}, T_{12}$, infer the type for $t_2$ and check that it is equal to $T_{11}$. If these checks hold, then we return $T_{12}$ as the type of the application.
So for knowing what $T_{11}$ is, it depends on what you're doing. If you're doing checking, then usually it is a type that has already been given to you. If you're doing inference, then you infer the type of the function, and inspect that type to verify that it's an arrow type, and can be broken into its parts. $T_{11}$ is one of these parts you break it into.
There's nothing saying you need to get $T_{11}$ only from the function's type. You could alternately infer it from the type of the argument, and then verify that it matched the function type.
The rules state what kinds of proofs are valid. No one ever promised it would always be easy to find a valid proof for any particular term of your choice. There may be multiple rules that could be used at any point; it's not the type rules' job to do anything about that.
Instead, that's the role of a type-checking algorithm. Depending on the type system, there may or may not be an efficient algorithm to find a valid proof (one that's deemed valid according to the rules), i.e., a valid sequence of rules to apply that proves the desired result.
You can't derive bottom up. It doesn't matter what T11 is. It's just some type; the rule holds no matter what it is. More precisely: if this is supposed to be a rule in a sequent calculus then I believe it is incomplete. The bottom sequent should have type annotations for every term. So you already have t11. Which suggests that jmite's answer is not quite right, insofar as it says we need to find some t11. But we dont, we're already given it in the premises, and the rule carries it over to the conclusion. If all you have is a,b:T, and you do not already know the types of a and b, you cannot infer them.
T11 is can be find on derivation on the right branch of that rule for type checking. On the right hand branch, you will eventually have
{x:T}|-x:T11
something like this. You apply "T_VAR" rule and get "T11=T". since above statement says, variable "x is type of T in syntax" there T should be equal to T11.
try some type checking, denote T11, then you see eventually T11 equals some type which is already known.
