### Edited by Fairouz Kamareddine

The first paper is by de Bruijn himself where he uses his experience of automating mathematics to reason about the human mind. Then, Barendregt proposes a mathematical proof language between informal and formalised mathematics which helps make proof assistants more user friendly. Then Constable explains how Automath's telescopes, books and definitions compare to recent developments in computational type theory made by his Nuprl group. Then Huet describes two design issues in symbolic computations and puts together convincingly two techniques which on the surface may seem unrelated: managing contexts and sharing. The article by Kamareddine, Laan and Nederpelt, studies the position of Automath within the framework of Pure Type Systems. The article of Franssen presents several ideas to design a Hoare Logic conforming to de Bruijn's criteria of a logic whose derivations are mechanically checked. The article of Arnon Avron argues that for automated reasoning, there is an interesting logic, somewhere strictly between first and second order logic, determined essentially by an analysis of transitive closure, yielding induction. The article of Randall Holmes presents a formal treatment and reports on an initial implementation of the ramified type theory used in Russell and Whitehead's Principia Mathematica. The paper of Ruiz-Reina etal, formalises and proves in the ACL2 theorem prover results concerning the multiset relation and other non-trivial mathematical theorems. The article of Gabbay presents a generalisation of Fraenkel-Mostowski (FM) set theory within higher-order logic, and applies it to model Milner's $\pi$-calculus. The article of Siekmann etal, presents a good overview and motivation of the $\Omega$mega system and discusses three different styles of proof development in $\Omega$mega using the example of the irrationality of $\sqrt 2$.