Universal algebra over lambda-terms and nominal terms
Murdoch J. Gabbay, Dominic P. Mulligan · 2009
This paper develops the correspondence between equality reasoning with axioms using λ-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: λ-terms represent functional abstraction; nominal terms represent atomsabstraction in nominal sets.