[Solved]: How to read typing rules?

In most type systems, the type rules work together to define judgements of the form: $$Gammavdash e:tau$$ This states that in context $Gamma$ the expression $e$ has type $tau$.
$Gamma$ is a mapping of the free variables of $e$ to their types. A type system will consist of a set of axioms and rules (a formal system of rules of inference, as Raphael points out). An axiom is of the form $$dfrac{}{Gamma vdash e:tau}$$ This states that the judgement $Gamma vdash e:tau$ holds (always). An example is $$dfrac{}{x:tauvdash x:tau}$$ which states that under the assumption that the type of variable $x$ is $tau$, then the expression $x$ has type $tau$. Inference rules take facts that have already been determined and build larger facts from them. For instance the inference rule $$dfrac{Gammavdash e_1:tautotau’ quad Gammavdash e_2:tau}{Gammavdash e_1 e_2:tau’}$$ says that if I have a derivation of the fact $Gammavdash e_1:tautotau’$ and a derivation of the fact $Gammavdash e_2:tau$, then I can obtain a derivation of the fact $Gammavdash e_1 e_2:tau’$. In this case, this is the rule for typing function application. There are two ways of reading this rule:

• top-down – given two expressions (a function and another expression) and some constraints on their type, we can construct another expression (the application of the function to the expression) with the given type.
• bottom-up – given an expression that is, in this case, the application of a function to some expression, the way this is typed is by first typing the two expressions, ensuring that their types satisfy some constraints, namely that the first is a function type and that the second has the argument type of the function.

Some inference rules also manipulate $Gamma$ by adding new ingredients into it (view-ed bottom up). Here is the rule for $lambda$-abstraction: $$dfrac{Gamma x:tauvdash e:tau’}{Gammavdash lambda x.e:tauto tau’}$$ The inference rules are applied inductively based on the syntax of the expression being considered to form a derivation tree. At the leaves of the tree (at the top) will be axioms, and branches will be formed by applying inference rules. At the very bottom of the tree is the expression you are interested in typing. For example, a derivation of the typing of expression $lambda f.lambda x.f x$ is $$dfrac{dfrac{}{f:tautotau’,x:tauvdash f:tautotau’} qquad dfrac{}{f:tautotau’,x:tauvdash}} {dfrac{f:tautotau’,x:tauvdash f x:tau’}{ dfrac{f:tautotau’vdash lambda x.f x:tau’}{vdash lambda f.lambda x.f x:tau’}}}$$ Two very good books for learning about type systems are:

• Types and Programming Languages by Benjamin Pierce
• Practical Foundations for Programming Languages by Robert Harper

Both books are very comprehensive, yet they start slowly, building a solid foundation.