Capture-avoiding substitution as a nominal algebra

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    17 Citations (Scopus)

    Abstract

    Substitution is fundamental to computer science, underlying for example quantifiers in predicate logic and beta-reduction in the lambda-calculus. So is substitution something we define on syntax on a case-by-case basis, or can we turn the idea of ‘substitution’ into a mathematical object? We exploit the new framework of Nominal Algebra to axiomatise substitution. We prove our axioms sound and complete with respect to a canonical model; this turns out to be quite hard, involving subtle use of results of rewriting and algebra.
    Original languageEnglish
    Title of host publicationTheoretical Aspects of Computing - ICTAC 2006 (Proceedings 3rd International Colloquium, Tunis, Tunisia, November 20-24, 2006)
    EditorsK. Barkaoui, A. Cavalcanti, A. Cerone
    Place of PublicationBerlin
    PublisherSpringer
    Pages198-212
    ISBN (Print)3-540-48815-4
    DOIs
    Publication statusPublished - 2006

    Publication series

    NameLecture Notes in Computer Science
    Volume4281
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Capture-avoiding substitution as a nominal algebra'. Together they form a unique fingerprint.

    Cite this