No label defined (Q4354787)

Nowadays, type theory has many applications and is used in a lot of different disciplines. Even within logic and mathematics, there are a lot of different type systems. They serve several purposes, and are formulated in various ways. In this thesis we present a formal framework in which various type theories can be described. This framework is an extension of an already existing framework. For the development of this framework, we follow the evolution of type theory throughout the past century. However, we do not only give a mere historical description. On the contrary: our goal is not to describe the various type systems that have been developed in their historical setting, but to present them in a modern framework. In this way it becomes clear how the various type systems are related to each other, even if originally those systems are described in very different ways. Moreover, we can make clear what is the essence, or the common basis, of the various modern type theories. The historical line in this thesis is, therefore, only part of our method of research, and definitely not a goal of our research.