A nominal axiomatisation of the lambda-calculus

M.J. Gabbay, A.H.J. Mathijssen

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

    13 Citaten (Scopus)


    The lambda calculus is fundamental in computer science. It resists an algebraic treatment because of capture-avoidance sideconditions. Nominal algebra is a logic of equality designed for specifications involving binding. We axiomatize the lambda calculus using nominal algebra, demonstrate how proofs with these axioms reflect the informal arguments on syntax and we prove the axioms to be sound and complete. We consider both non-extensional and extensional versions (alpha-beta and alpha-beta-eta equivalence). This connects the nominal approach to names and binding with the view of variables as a syntactic convenience for describing functions. The axiomatization is finite, close to informal practice and it fits into a context of other research such as nominal rewriting and nominal sets.
    Originele taal-2Engels
    Pagina's (van-tot)501-531
    TijdschriftJournal of Logic and Computation
    Nummer van het tijdschrift2
    StatusGepubliceerd - 2010


    Duik in de onderzoeksthema's van 'A nominal axiomatisation of the lambda-calculus'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit