This thesis consists of two separate parts. In part I we prove a number smaller results concerning a class of types in the polymorphic lambda calculus (system F) which we refer to as Pi-1 types. These are the types where the occurrences of the quantifier Pi have "even depth". In particular, we give three alternative proofs that inhabitation is decidable and show that the Pi-1 types of increasing quantifier depth form a hierarchy. We also show that the interpretations of such types is well-behaved in the standard PER model but not in general PER models.
In part II the scope is much wider. First we construct a logical framework, called SFL, and establish various basic properties such as a form of normalization. We also show how various deductive systems can be formalized in this framework; in particular how SFL can be formalized in itself. However, SFL can not only be used to formalize deductive systems given in advance. It is much clearer to formalize complex constructions such as quotient types directly in SFL; so in the next chapter we give formalizations in SFL of a long list of "standard operators".
Some of these operators are used to give a refined formalization of SFL in itself, a valuable tool for obtaining various meta-results. In particular, it is used to develop an abstract theory of logical relations and explain how types can be "simulated" in untyped theories such as Heyting arithmetic. Finally, we consider SFL extended with an abstract notion of sets, and show how it can be used to reason about a variety of structures as if they were sets. This also leads to a better understanding of traditional set theories such as ZF.