Add to ORKGDedicated to the memory of Ole-Johan Dahl Abstract. 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 p...