To paraphrase the correspondence, proving Γ ⊢ "α" means having a program that, given values with the types listed in Γ, manufactures an object of type "α". An axiom corresponds to the introduction of a new variable with a new, unconstrained type, the rule corresponds to function abstraction and the rule corresponds to function application. Observe that the correspondence is not exact if the context Γ is taken to be a set of formulas as, e.g., the "λ"-terms "λx"."λy"."x" and "λx"."λy"."y" of type would not be distinguished in the correspondence. Examples are given below.