Pure Type Systems, Cut, and Explicit Substitution
                Romain Kervarc and Pierre Lescanne

Pure type systems are a general formalism allowing to represent many
type systems ­ in particular, Barendregt's lambda-cube, including
Girard's system F, dependent types, and the calculus of constructions.
We built a variant of pure type systems by adding a cut rule
associated to an explicit substitution in the syntax, according to the
Curry-Howard-de Bruijn correspondence.  The addition of the cut
requires the addition of a new rule for substitution, with which we
are able to show type correctness and subject reduction for all
explicit systems. Moreover, we proved that the explicit lambda-cube
obtained this way is strongly normalizing.