Unity in nominal equational reasoning: The algebra of equality on nominal sets

Bourbaki, 1970 Calvès, 2008, Nominal matching and alpha-equivalence, vol. 5110 Calvès, 2008, A polynomial nominal unification algorithm, Theoretical Computer Science, 403, 285, 10.1016/j.tcs.2008.05.012 Cheney, 2008, Nominal logic programming, ACM Transactions on Programming Languages and Systems (TOPLAS), 30, 1, 10.1145/1387673.1387675 Ranald Clouston, Equational logic for names and binding, PhD thesis, University of Cambridge, UK, 2009. Clouston, 2010, Binding in nominal equational logic, vol. 265 Clouston, 2011, Nominal Lawvere theories, vol. 6642 Clouston, 2007, Nominal equational logic, vol. 172, 223 Cohn, 1965 de Bruijn, 1972, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church–Rosser theorem, Indagationes Mathematicae, 5, 381, 10.1016/1385-7258(72)90034-0 Gilles Dowek, Murdoch J. Gabbay, Permissive nominal logic, in: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2010, 2010, pp. 165–176. Gilles Dowek, Murdoch J. Gabbay, Permissive nominal logic (journal version), Transactions on Computational Logic (2012), in press, http://tocl.acm.org/accepted.html. Gilles Dowek, Murdoch J. Gabbay, Dominic P. Mulligan, Permissive nominal terms and their unification, in: Proceedings of the 24th Italian Conference on Computational Logic (CILCʼ09), 2009. Dowek, 2010, Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques (journal version), Logic Journal of the IGPL, 18, 769, 10.1093/jigpal/jzq006 Fernández, 2007, Nominal rewriting (journal version), Information and Computation, 205, 917, 10.1016/j.ic.2006.12.002 Fernández, 2004, Nominal rewriting systems, 108 Fiore, 2008, Term equational systems and logics, Electronic Notes in Theoretical Computer Science, 218, 171, 10.1016/j.entcs.2008.10.011 Gabbay, 2005, Axiomatisation of first-order logic (talk) Gabbay, 2009, Nominal algebra and the HSP theorem, Journal of Logic and Computation, 19, 341, 10.1093/logcom/exn055 Gabbay, 2009, A study of substitution, using nominal techniques and Fraenkel–Mostowski sets, Theoretical Computer Science, 410, 1159, 10.1016/j.tcs.2008.11.013 Gabbay, 2011, Foundations of nominal techniques: logic and semantics of variables in abstract syntax, Bulletin of Symbolic Logic, 17, 161, 10.2178/bsl/1305810911 Gabbay, 2012, Nominal terms and nominal logics: from foundations to meta-mathematics, vol. 17 Gabbay, 2012, Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free, Journal of Symbolic Logic, 10.2178/jsl/1344862164 Murdoch J. Gabbay, Aad Mathijssen, Nominal algebra, in: 18th Nordic Workshop on Programming Theory, October 2006. Gabbay, 2008, Nominal renaming sets, 158 Gabbay, 2006, One-and-a-halfth-order logic, 189 Gabbay, 2006, Capture-avoiding substitution as a nominal algebra, vol. 4281, 198 Gabbay, 2007, A formal calculus for informal equality with binding, vol. 4576, 162 Gabbay, 2008, One-and-a-halfth-order logic, Journal of Logic and Computation, 18, 521, 10.1093/logcom/exm064 Gabbay, 2009, Nominal universal algebra: equational logic with names and binding, Journal of Logic and Computation, 19, 1455, 10.1093/logcom/exp033 Gabbay, 2010, A nominal axiomatisation of the lambda-calculus, Journal of Logic and Computation, 20, 501, 10.1093/logcom/exp049 Gabbay, 2009, Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables, 64 Gabbay, 2001, A new approach to abstract syntax with variable binding, Formal Aspects of Computing, 13, 341 Henkin, 1971 Hodges, 1993 Kurz, 2010, On universal algebra over nominal sets, Mathematical Structures in Computer Science, 20, 285, 10.1017/S0960129509990399 Levy, 2010, An efficient nominal unification algorithm, vol. 6, 209 Levy, 2011, Nominal unification from a higher-order perspective, Transactions on Computational logic (TOCL), 13 Pfenning, 1988, Higher-order abstract syntax, 199 Urban, 2004, Nominal unification, Theoretical Computer Science, 323, 473, 10.1016/j.tcs.2004.06.016