Masahiko Sato, from SCSS 2009, available from Masahiko Sato’s webpage:
It is well known that defining the substitution operation on λ-terms appropriately and establish basic properties like the substitution lemma is a subtle task if we wish to do it formally. The main obstacle here comes from the fact that unsolicited capture of free variables may occur during the substitution if one defines the operation naively.
We argue that although there are several approaches to cope with this problem, they are all unsatisfactory since each of them defines the λ- terms in terms of a single fixed syntax. We propose a new way of defining λ-terms which uses an external syntax to be used mainly by humans and an internal syntax which is used to implement λ-terms on computers.
In this setting, we will show that we can define λ-terms and the substitution operation naturally and can establish basic properties of terms easily.
Slides from a talk covering related work with Randy Pollack, presented at TAASN 2009, are available from Randy Pollack’s website.