Keywords: Pure Type Systems, Logical Framework, Calculus of Constructions, Higher Order Logic, Typed Lambda Calculus, Rewriting Logic
Pure type systems (PTS) generalize the lambda-cube, which already contains important systems, like the simply typed and the (higher-order) polymorphic lambda calculi, a system LP close to the logical framework LF, and their combination, the calculus of constructions CC. PTS systems are considered to be of key importance, since their generality and simplicity makes them an ideal basis for representing higher-order logics either directly, via the propositions-as-types interpretation, or via their use as a logical framework. In  we show how the definition of PTS systems can be formalized in membership equational logic. It is noteworthy that the representational distance between the informal mathematical presentation of PTS systems with identification of alpha-equivalent terms and the membership equational logic specification of PTS systems is close to zero. In contrast to a higher-order representation in LF or Isabelle, this first-order inductive approach is closer to mathematical practice, and the adequacy of the representation does not require complex meta-logical justifications. It has also greater explanational power, since we explain higher-order calculi in terms of a first-order system with a very simple semantics.
We have also introduced uniform pure type systems (UPTS) a more concrete variant of PTS systems that do not abstract from the treatment of names, but use a uniform notion of names based on CINNI , a new first-order calculus of names and substitutions. UPTS systems solve the problem of closure under alpha-conversion, that has been discussed by Pollack (1993) and also encountered by Magnussen (1994), in a very elegant way. A membership equational logic specification of UPTS systems can be given that contains the equational substitution calculus and directly formalizes the informal presentation.
Furthermore, the reference  describes how meta-operational aspects of UPTS systems, like type checking and type inference, can be formalized in rewriting logic. For this purpose the inference system of a UPTS system is specified as a rewrite theory. The result of this formalization is an executable specification of UPTS systems that is correct w.r.t. the more abstract specification in a very obvious way.