Reynolds: "the basic laws of variable binding" I recently came across this passage in an article by John Reynolds (emphasis added):


  ...from designers innocent of the principles of programming language design, we have been given a nearly endless succession of “input formats” that seem to be designed to encourage error. (Flawed macro facilities that violate the basic laws of variable binding are particularly prominent examples.)


I was happy to come across the phrase in italics because for some time now I've been aware of having precisely this deficiency, but not knowing what to call it, and therefore failing repeatedly at finding a way to remedy it.

Can someone point me to where I can learn about these "basic laws of variable binding"?
See chapter 1 of Robert Harper's book Practical Foundations of Programming Languages. He formalizes syntax with binding operators using the notion of "abstract binding trees", which IIRC were originally introduced in the Nuprl proof assistant. The main keyword you need to find further information is "alpha-equivalence".