Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath (Q701700)

The articles of this volume will be reviewed individually. Indexed articles: \textit{de Bruijn, N. G.}, A mathematical model for biological memory and consciousness, 9-23 [Zbl 1180.92016] \textit{Barendregt, Henk}, Towards an interactive mathematical proof mode, 25-36 [Zbl 1063.68088] \textit{Constable, Robert L.}, Recent results in type theory and their relationship to Automath, 37-48 [Zbl 1063.68090] \textit{Huet, Gérard}, Linear contexts, sharing functors: techniques for symbolic computation, 49-69 [Zbl 1063.68109] \textit{Kamareddine, Fairouz; Laan, Twan; Nederpelt, Rob}, De Bruijn's Automath and pure type systems, 71-123 [Zbl 1063.68092] \textit{Franssen, Michael}, Hoare logic with explicit contexts, 125-148 [Zbl 1063.68031] \textit{Holmes, M. Randall}, Polymorphic type-checking for the ramified theory of types of \textit{Principia mathematica}, 173-215 [Zbl 1063.68091] \textit{Ruiz-Reina, J. L.; Alonso, J. A.; Hidalgo, M. J.; Martín-Mateos, F. J.}, Termination in ACL2 using multiset relations, 217-245 [Zbl 1063.68026] \textit{Gabbay, Murdoch J.}, The \(\pi\)-calculus in FM, 247-269 [Zbl 1063.68073] \textit{Siekmann, Jörg; Benzmüller, Christoph; Fiedler, Armin; Meier, Andreas; Normann, Immanuel; Pollet, Martin}, Proof development with \(\Omega\)MEGA: the irrationality of \(\sqrt 2\), 271-314 [Zbl 1063.68093]