@inbook{0041ee9c317c4a4491e65d468ffb9868,
title = "A verifying program for Automath",
abstract = "This paper describes the Automath verifier which is being operated [in the beginning of the seventies] at the Technological University at Eindhoven. The description is given in terms of a number of procedures, written in an ALGOL-like language. The contents are: 1. General remarks. 2. The description language. 3. The translator. 4. Some basic notions and procedures. 5. Substitution. 6. Reductions. 7. CAT and DOM. 8. Definitional equality. 9. Correctness of expressions. 10. Correctness of lines. 11. A paragraph system. 12. Final remarks.\ For the theoretical background we refer to the papers of Prof. de Bruijn, D. van Daalen and R. Nederpelt: [de Bruijn 70a (AS)], [de Bruijn 73b], [van Daalen 73 (A.3)] and [Nederpelt 73 (CS)].",
author = "I. Zandleven",
year = "1994",
language = "English",
isbn = "0-444-89822-0",
series = "Studies in Logic",
publisher = "North-Holland Publishing Company",
pages = "783--804",
editor = "R.P. Nederpelt and J.H. Geuvers and {Vrijer, de}, R.C.",
booktitle = "Selected Papers on Automath",
address = "Netherlands",
}