A verifying program for Automath

I. Zandleven

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    Abstract

    This paper describes the Automath verifier which is being operated [in the beginning of the seventies] at the Technological University at Eindhoven. The description is given in terms of a number of procedures, written in an ALGOL-like language. The contents are: 1. General remarks. 2. The description language. 3. The translator. 4. Some basic notions and procedures. 5. Substitution. 6. Reductions. 7. CAT and DOM. 8. Definitional equality. 9. Correctness of expressions. 10. Correctness of lines. 11. A paragraph system. 12. Final remarks.\ For the theoretical background we refer to the papers of Prof. de Bruijn, D. van Daalen and R. Nederpelt: [de Bruijn 70a (AS)], [de Bruijn 73b], [van Daalen 73 (A.3)] and [Nederpelt 73 (CS)].
    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
    Pages783-804
    ISBN (Print)0-444-89822-0
    Publication statusPublished - 1994

    Publication series

    NameStudies in Logic
    Volume133

    Fingerprint Dive into the research topics of 'A verifying program for Automath'. Together they form a unique fingerprint.

    Cite this