The AUTOMATH family of languages can be viewed as typed lambda-calculi. The type structures are parameterized and highly complex, as befits the fact that propositions are types, the elements of which are the proofs of that proposition. A description of AUTOMATH can be found in [1].

This paper provides a formal semantics for many of the AUTOMATH languages, based on a mapping into the type-free lambda calculus. The core of the paper is eight pages of type-free lambda calculus, followed by an eight-page description of Classical AUTOMATH culminating in an “obvious” Soundness Theorem for Classical AUTOMATH. The material is extremely technical and not very well motivated, and the reviewer confesses that he does not follow all the details. The result is clearly relevant for much of the theory of higher-order languages. There is an interesting discussion of the limitations of this method, which unfortunately relies heavily on PhD theses and technical reports.