(eng) Pure type systems are an elegant formalism allowing to specify in a very easy way a large number of type systems. The possibility of their extension to calculi with explicit substitution was the object of numerous ...