I was wondering if the sorts of things that Andrew Pitts and Jamie Gabbay do on fresh names could be applied easily to anaphora effects. Hmmm. Reminder of what anaphora are (see Anaphora at the Stanford Encyclopedia of Philosophy). Take the sentence
John left. He said he was ill.
The pronoun “he” is said to inherent its referent from “John”, the antecedent. Another example:
Every male lawyer believes he is smart.
This is close to universal quantification: forall x. Male x & Lawyer x => … So the antecedent here is a bound variable.
Pitts says on his web page that he is
currently researching nominal sets, which provide a syntax-independent model of freshness and α-equivalence of bound names with very good support for recursion and induction.
I will try to develop this further once I get back from Malta…