A Major complication in programming with higher-order abstract syntax is that recursion over such encodings requires one to traverse a lambda-abstraction and hence necessitates reasoning about "open" objects.  I present a novel approach based on contextual modal types which overcomes these difficulties and allows recursion over open terms. In addition, it also supports first-class substitutions and contexts.

I will present some examples to motivate the approach and highlight the differences with existing approaches, and then present a bi-directional type system together with progress and preservation proofs. Finally, if time permits, I will talk about some open problems.

Principles of Programming Seminars