An interesting view of programming languages is as a tractable approximation to the intractably rich world of foundational type theories, in which the whole of mathematics can be performed. New programming language developments often result from mapping type-theoretic constructions through an approximation into a programming language setting, and, conversely, new paradigms in programming languages are often not well understood until they have been formulated type-theoretically. I am interested in deepening our understanding of this relationship between type theory and programming languages, particularly the issues of tractability and approximation and how they can be mitigated.
I am also interested in a model of compilation that views it as a series of translations into "lower" intermediate calculi, where each intermediate calculus can be embedded into type theory and the corresponding interpretation of a program is invariant under each translation. Such a model allows us to relate each stage of compilation to an original type-theoretic semantics, which allows the use of standard compilation techniques and optimizations while guaranteeing safety and correctness. Also, careful formulation of such intermediate calculi make possible additional optimizations that are unavailable in other compilation strategies.
My work forms part of the Nuprl project here at Cornell. The project name comes from the Nuprl system of formal mathematics and logic, a type theory based on the type theories of Martin-Löf that is also implemented in an automated reasoning system.
My committee consists of Robert Constable, Greg Morrisett, and Dexter Kozen. I also work closely with Jason Hickey.
"Of all the commandments, which is the most important?""The most important one," answered Jesus, "is this: 'Hear, O Israel, the Lord our God, the Lord is one. Love the Lord your God with all your heart and with all your soul and with all your mind and with all your strength.' The second is this: 'Love your neighbor as yourself.' There is no commandment greater than these."
-- Mark 12:29-31