De Bruijn's Automath and pure type systems

F. Kamareddine, T.D.L. Laan, R.P. Nederpelt

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review


We study the position of the Automath systems within the framework of Pure Type Systems (PTSs). In [2, 22], a rough relationship has been given between Automath and PTSs. That relationship ignores three of the most important features of Automath: definitions, parameters and -reduction, because at the time, formulations of PTSs did not have these features. Since, PTSs have been extended with these features and in view of this, we revisit the correspondence between Automath and PTSs. This paper gives the most accurate description of Automath as a PTS so far.
Original languageEnglish
Title of host publicationThirty Five Years of Automating Mathematics
EditorsF.D. Kamareddine
Place of PublicationDordrecht
PublisherKluwer Academic Publishers
ISBN (Print)1-4020-1656-5
Publication statusPublished - 2003

Publication series

NameApplied Logic Series
ISSN (Print)1386-2790


Dive into the research topics of 'De Bruijn's Automath and pure type systems'. Together they form a unique fingerprint.

Cite this