A description of Automath and some aspects of its language theory

D.T. van Daalen

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    2 Citations (Scopus)


    definition and an overview of the language theory. Thus it can serve as an introduction to the papers [van Benthem Jutting 73] and [Zandlevem 73 (E.1)]. Among the various Automath languages this paper concentrates on the original version AUT-68 (because of its relative simplicity) and one extension AUT-QE (in which most texts have been written thus far). The contents are: 1. Introductory remarks. 2. Informal description of AUT-68. 3. Mathematics in Automath: propositions and types. 4. Extension of AUT-68 to AUT-QE. 5. A formal definition of AUT-QE. 6. Some remarks on language theory.
    Original languageEnglish
    Title of host publicationSelected Papers on Automath
    EditorsR.P. Nederpelt, J.H. Geuvers, R.C. Vrijer, de
    Place of PublicationAmsterdam
    PublisherNorth-Holland Publishing Company
    ISBN (Print)0-444-89822-0
    Publication statusPublished - 1994

    Publication series

    NameStudies in Logic


    Dive into the research topics of 'A description of Automath and some aspects of its language theory'. Together they form a unique fingerprint.

    Cite this