Reasoning about Languages with Binding: a first-order foundation and full adequacy

We will look at what is involved in formally proving results about languages with binding. We will in particular focus on what we want to prove, what we actually do prove, and what requirements we need to put on the formalisms that we use.