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 [4] 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
[1], 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 [4] 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.

Relevant References:

- Mark-Oliver Stehr:
*CINNI - A New Calculus of Explicit Substitutions and its Application to Pure Type Systems*, Manuscript, CSL, SRI-International, Menlo Park, CA, USA, May 1999 - Manuel Clavel, Francisco Duran, Steven Eker, Jose Meseguer,
Mark-Oliver Stehr:
*Maude as a Formal Meta-Tool.*In the proceedings of FM'99, The World Congress On Formal Methods. Toulouse, France, September 20-24, 1999. Also appeared in the book*OBJ/CafeOBJ/Maude at Formal Methods '99,*Kokichi Futatsugi, Joseph Goguen and Jose Meseguer (Eds.), Theta (Bucharest), September 1999, ISBN 973-99097-1-X. - Mark-Oliver Stehr:
*Type Theory in a Membership Equational Logic Framework*(Talk given at Cornell) - Mark-Oliver Stehr, Jose Meseguer:
*Pure Type Systems in Rewriting Logic*, Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999. Paper available here . Extended version submitted for publication.