This talk will describe some recent joint work I've been doing with Andy Gordon on reasoning in a theorem prover about languages whose syntax includes name-binding operators. Previous experience suggests that developing theories of, for example, substitution in the presence of binding operators is a tedious and error-prone business. We advocate first developing a metatheory of untyped lambda-terms, and then deriving syntax for a particular programming language as abbreviations for untyped lambda-terms. The motivation is similar to that of higher order abstract syntax, but our proposal is technically quite different.
As a beginning, we have developed an abstractly-specified theory (in HOL) of name-carrying lambda-terms identified up to alpha-conversion. We are now experimenting with applications of our theory. This talk will provide an overview of the overall research programme, its motivation, and the current state of our progress.