By Edwin Westbrook, from TFP 2006, available from Aaron Stump’s website:
Higher-order abstract syntax (HOAS) has been shown to be useful in formal systems for reasoning about programming languages. How to recurse over HOAS representations, however, is a well-known problem. This is because, in most current systems, it is generally impossible to recurse on the body of a λ-abstraction without creating a fresh variable, which must itself be bound. This in turn makes it impossible, for instance, to extract first-order data from higher-order data. One previous approach to this problem has been to allow the creation of fresh variables that are not bound to pass to λ-abstractions as long as they can be shown not to escape their scope. Current systems cannot show these do not escape their scope without a runtime check. In this paper, we propose a novel type system that allows explicit reasoning about free variables. This type system can ensure these fresh variables do not escape their scopes without runtime checks. The usefulness of this approach is shown with a simple example.