Generalizing Automath by means of a lambda-typed lambda calculus

N.G. Bruijn, de

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    2 Citations (Scopus)
    56 Downloads (Pure)

    Abstract

    The calculus delta conjunction developed in this paper is claimed to be able to embrace all the essential aspects of Automath, apart from the feature of type inclusion which will not be considered in this paper. The calculus deal with a correctness notion for lambda-typed lambda formulas (which are presented in the form of what will be called lambda trees). To an automath book there corresponds a single lambda tree. and the correcntess of the book is equivalent to the correctness of the tree. The algorithmic definition of correctness of lambda trees corresponds to an efficient checking algorithm for Automath Books
    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
    Pages313-337
    ISBN (Print)0-444-89822-0
    Publication statusPublished - 1994

    Publication series

    NameStudies in logic and the foundations of mathematics
    Volume133
    ISSN (Print)0049-237X

    Cite this