Characteristics of de Bruijn’s early proof checker Automath

Article type: Research Article

Authors: Geuvers, Herman^{; *} | Nederpelt, Rob

Affiliations: Radboud University Nijmegen and Eindhoven University of Technology, Nijmegen, The Netherlands. herman@cs.ru.nl | Eindhoven University of Technology, Nijmegen, The Netherlands

Correspondence: [*] Address of correspondence: H. Geuvers, Faculty of Science, Radboud University, PO Box 9010, 6500 GL Nijmegen, The Netherlands.

Abstract: The ‘mathematical language’ Automath, conceived by N.G. de Bruijn in 1968, was the first theorem prover actually working and was used for checking many specimina of mathematical content. Its goals and syntactic ideas inspired Th. Coquand and G. Huet to develop the calculus of constructions, CC ([1]), which was one of the first widely used interactive theorem provers and forms the basis for the widely used Coq system ([2]). The original syntax of Automath ([3, 4]) is not easy to grasp. Yet, it is essentially based on a derivation system that is similar to the Calculus of Constructions (‘CC’). The relation between the Automath syntax and CC has not yet been sufficiently described, although there are many references in the type theory community to Automath. In this paper we focus on the backgrounds and on some uncommon aspects of the syntax of Automath. We expose the fundamental aspects of a ‘generic’ Automath system, encapsulating the most common versions of Automath. We present this generic Automath system in a modern syntactic frame. The obtained system makes use of λD, a direct extension of CC with definitions described in [5].

DOI: 10.3233/FI-222112

Journal: Fundamenta Informaticae, vol. 185, no. 4, pp. 313-336, 2022