Capture-avoiding substitution as a nominal algebra

Murdoch Gabbay, Aad Mathijssen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. © Springer-Verlag Berlin Heidelberg 2006.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2006 Third International Colloquium, Proceedings
Pages198-212
Number of pages15
Volume4281 LNCS
Publication statusPublished - 2006
EventThird International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings - Tunis, Tunisia
Duration: 20 Nov 200624 Nov 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4281 LNCS
ISSN (Print)0302-9743

Conference

ConferenceThird International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings
CountryTunisia
CityTunis
Period20/11/0624/11/06

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

Cite this