In Comparing Mathematical Provers (section 4.1), Wiedijk classifies logics and type systems of different proof assistants? I do not see what he means by type system of the assistant. He only says:
A system is only considered typed when the types are first class objects that occur in variable declarations and quantifiers.
I can only think of types in goals. For instance, in Isabelle if you write a goal using variables (I don't think you "declare" variables", you can check the type of these variables. But this type is certainly a type in the logic I'm using.
It would be interesting to clarify this and apply this example in the cases of Isabelle, Coq and Metamath (which is untyped and apparently based on proof trees, which could give a hint).
