A verifying program for Automath

I. Zandleven

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademic

    1 Citaat (Scopus)

    Samenvatting

    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)].
    Originele taal-2Engels
    TitelSelected Papers on Automath
    RedacteurenR.P. Nederpelt, J.H. Geuvers, R.C. Vrijer, de
    Plaats van productieAmsterdam
    UitgeverijNorth-Holland Publishing Company
    Pagina's783-804
    ISBN van geprinte versie0-444-89822-0
    StatusGepubliceerd - 1994

    Publicatie series

    NaamStudies in Logic
    Volume133

    Vingerafdruk

    Duik in de onderzoeksthema's van 'A verifying program for Automath'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit