Brigitte Pientka
McGill University

Functional Programming with HOAS


Abstract:

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.
Host:  Frank Pfenning
Appointments: Frank Pfenning <fp@cs.cmu.edu>


Friday, May 4, 2007
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars