Selected Papers on Automath

Part A: 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 B: 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 C: Theory. A normal form theorem in a &lgr;-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 &lgr;-calculus with &lgr;-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 &Lgr;∞, a typed &lgr;-calculus where terms are typed (L.S. van Benthem Jutting). Part D: 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, 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 E: 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 &lgr;-calculus with dependent types (L.S. van Benthem Jutting). Part F: 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). Computer program semantics in space and time (N.G. de Bruijn). Bibliography. Indexes.