Pure type systems in rewriting logic: Specifying typed higher-order languages in a first-order logical framework

The logical and operational aspects of rewriting logic as a logical framework are tested and illustrated in detail by representing pure type systems as object logics. More precisely, we apply membership equational logic, the equational sublogic of rewriting logic, to specify pure type systems as they can be found in the literature and also a new variant of pure type systems with explicit names that solves the problems with closure under α-conversion in a very satisfactory way. Furthermore, we use rewriting logic itself to give a formal operational description of type checking, that directly serves as an efficient type checking algorithm. The work reported here is part of a more ambitious project concerned with the development of the open calculus of constructions, an equational extension of the calculus of constructions that incorporates rewriting logic as a computational sublanguage.