D. Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. Studies in logic and the foundations of mathematics, 133:73-100, 1970. [doi]
S2 TL;DR: The possibilities of superimposed languages, automatic theorem proving, and extensions of Automath are described in this chapter.