A nominal axiomatisation of the lambda-calculus

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

    Research output: Contribution to journalArticleAcademicpeer-review

    13 Citations (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.
    Original languageEnglish
    Pages (from-to)501-531
    JournalJournal of Logic and Computation
    Issue number2
    Publication statusPublished - 2010


    Dive into the research topics of 'A nominal axiomatisation of the lambda-calculus'. Together they form a unique fingerprint.

    Cite this