Proof Rules for Typing -Terms

We want to establish a connection between types and -terms. This is done by introducing typing rules. First we define a typing environment.

Any typing derivation can be done using the following three rules. You can see that we state all the rules of typing with respect to an environment.

1. Projection rule (or axiom):

   The symbol is used only for declarations of variables, in a way similar to what we find in programming languages. Whenever you see a colon, you know that the term on the left hand side is a variable, and the one on the right is a type. The symbol is used more generally, when we have on the left hand side a term, and on the right a type.

2. Abstraction rule:
   

   We start with an old environment , and we declare the type of the bound variable to be . If in the new environment which results by adding to the new typing we can show that the body of has type , then we know that in , the old environment, the abstraction has the type .

3. Application rule:
   

   If we can show in the environment that has type , and we can show in that has type (), then we can infer that in that the application of to has type .

We need that abstarction rule be a little stronger. So that we can take care of bound variables properly. The modified version of the rule is :

where is a fresh variable not occurring in or in .