Selected Papers on Automath

Part 1 Motivation and exposition: verification of mathematical proofs by a computer, N.G. de Bruijn; the mathematical language automath, its usage, and some of its extensions, N.G. de Bruijn; a description of automath and some aspects of its language theory, D.T. van Daalen; formalization of classical mathematics in automath, J. Zucker; a survey of the project automath, N.G. de Bruijn; the language theory of automath; chapter I, sections 1-5 (introduction), D.T. van Daalen; reflections on automath, N.G. de Bruijn; type systems - basic ideas and applications, R.P. Nederpelt. Part 2 Language definition and special subjects: description of AUT-68, L.S. van Benthem Jutting; AUT-SL, a single line version of automath, N.G. de Bruijn; some extensions of automath - the AUT-4 family, N.G. de Bruijn; AUT-QE without type inclusion, N.G. de Bruijn; checking Landau's "Grundlagen" in the automath system; appendix 9 (AUT-SYNT), L.S. van Benthem Jutting; the language theory of automath; chapter VIII, 1 and 2 (AUT-II), D.T. van Daalen; generalizing automath by means of a lambda-typed lambda calculus, N.G. de Bruijn; lambda calculus extended with segments; chapter 1, sections 1.1 and 1.2 (introduction), H. Balsters. Part 3 Theory: a normal form theorem in a ?????-calculus with types, L.S. van Benthem Jutting; lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, N.G. de Bruijn; strong normalization in a typed lambda calculus with lambda structured types, R.P. Nederpelt; big trees in a ?????-calculus with ?????-expressions as types, R.C. de Vrijer; the language theory of automath; parts of chapters II, IV, V-VIII, D.T. van Daalen; the language theory of ?????, a typed ?????-calculus where terms are typed, L.S. van Benthem Jutting. Part 4 Text examples: example of a text written in automath, N.G. de Bruijn; checking Landau's "Grundlagen" in the automath system; parts of chapters 0, 1 and 2 (introduction, preparation, translation), L.S. van Benthem Jutting; checking landau's "Grundlagen" in the automath system; chapter 4 (conclusions), L.S. van Benthem Jutting; a text fragment from Zucker's "Real analysis", L.S. van Benthem Jutting and R.C. de Vrijer; checking Landau's "Grundlagen" in the automath system; appendices 3 and 4 (the PN-lines; excerpt for "Satz 27", L.S. van Benthem Jutting. Part 5 Verification: a verifying program for automath, I. Zandleven; checking Landau's "Grundlagen" in the automath system; parts of chapter 3 (verification), L.S. van Benthem Jutting; an implementation of substitution in a ?????-calculus with dependent types, L.S. van Benthem Jutting. Part 6 Related topics: set theory with type restrictions, N.G. de Bruijn; formalization of constructivity in automath, N.G. de Bruijn; the mathematical vernacular, a language for mathematics with typed sets, N.G. de Bruijn; relational semantics in an integrated system, R.M.A. Wieringa; (Part contents)