Based on old work (with James McKinna) on formalising the theory of PTS in LEGO, and recent work formalizing my TLCA'03 paper (with Thierry Coquand and Makoto Takeyama) in Coq, I'm interested again in the problem of reasoning about languages with binding. New papers about approaches to this problem seem to appear every year. Do any of these approaches make it feasible to formalize your latest paper? What are the real difficulties, and where do each of the approaches fall down?

As examples that seem difficult to formalize in various approaches, I will present parts of the semantics of a logical framework developed in my TLCA'03 paper. This example is interesting in itself, as our semantics follows closely Martin-Löf's meaning explanation, with a semantics for categorical judgements, then extended to hypothetical judgements.

An informal collaboration wants to develop a "challenge problem set" to help evaluate the various approaches for formalizing binding. If you have encountered (or overcome) problems in this area, I want to hear about it.