Pure Type Systems with de Bruijn indices

Nowadays, type theory has many applications and is used in many different disciplines. Within computer science, logic and mathematics there are many different type systems. They serve several purposes and are formulated in various ways. A general framework called Pure Type Systems (PTSs) has been introduced independently by Terlouw and Berardi in order to provide a unified formalism in which many type systems can be represented. In particular, PTSs allow the representation of the simple theory of types, the polymophic theory of types, the dependent theory of types and various other well-known type systems such as the Edinburgh Logical Frameworks and the Automath system. PTSs are usually presented using variable names. In this article, we present a formulation of PTSs with de Bruijn indices. De Bruijn indices avoid the problems caused by variable names during the implementation of type systems. We show that PTSs with variable names and PTSs with de Bruijn indices are isomorphic. This isomorphism enables us to answer questions about PTSs with de Bruijn indices including confluence, termination (strong normalization) and safety (subject reduction).