Automath

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.
(Introduction copied from the website, hope that is allowed).

Ehud, I hope this satisfies your wish for historical CS subjects.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

But you should become an

But you should become an editor to make life easier for me by posting directly to the home page...

Can you tell me how to

Can you tell me how to become an editor.

It is a simple procedure:

It is a simple procedure: You send me an email, and I sign you up...