@inproceedings{f574348c6bdc4bab9f89fff84b399071,

title = "Capture-avoiding substitution as a nominal algebra",

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 {\textquoteleft}substitution{\textquoteright} 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.",

author = "M.J. Gabbay and A.H.J. Mathijssen",

year = "2006",

doi = "10.1007/11921240_14",

language = "English",

isbn = "3-540-48815-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "198--212",

editor = "K. Barkaoui and A. Cavalcanti and A. Cerone",

booktitle = "Theoretical Aspects of Computing - ICTAC 2006 (Proceedings 3rd International Colloquium, Tunis, Tunisia, November 20-24, 2006)",

address = "Germany",

}