| Welcome to The Automath Archive |
| The Automath Archive was created
by the Brouwer Institute in Nijmegen and the Formal Methods section of Eindhoven
University of Technology. Started by prof. H. Barendregt, in cooperation
with Rob Nederpelt, this archive project was launched to digitize valuable
historical articles and other documentation concerning the Automath project. Initiated by prof. N.G. de Bruijn, the project Automath (1967 until the early 80's) aimed at designing a language for expressing complete mathematical theories in such a way that a computer can verify the correctness. This project can be seen as the predecessor of type theoretical proof assistants such as the well known Nuprl and Coq. |
 |
|
|
In 1994 a compilation of a number
of papers about Automath appeared in 'Selected Papers on Automath', which
now is the standard reference about the subject. While some of the articles
related to the Automath project are published elsewhere, many interesting
other parts of the documentation remained unavailable to the scientific
world. In honour of prof. N.G. de Bruijn's 85th birthday in 2003, we started to investigate the paper archive of the Automath project that is still present at Eindhoven University, and to digitize a number of articles and other documentation. As a result, they are now available here, in this online archive. |
| We aim to make these documents, deposited by the Eindhoven University of Technology, accessible via the internet. For the first time one can access almost 200 documents related to the Automath project. |
