Sabine Broda
After an introduction to the main basic facts and properties of the simply typed lambda calculus we focus on several aspects concerning (principal) inhabitation. Here we present an alternative representation of types, called formula-trees, that clarifies the relationship between the structure of a type and its normal inhabitants, or equivalently between the structure of formulas in the implicational fragment of intuitionistic propositional logic and the structure of their normal proofs in the natural deduction system. Based on this alternative representation of types we introduce the formula-tree proof method (a short presentation of this method together with an implementation as a Java applet can be found at http://www.ncc.up.pt/~ sbb/FTLab/ftlab) and illustrate the adequateness of the method in this area with various applications, such as counting algorithms, description of the set of normal inhabitants of a type by a context-free grammar, results concerning provability in implicational intuitionistic logic, etc.