I am interested in the application of type theory to the implementation of modern type-safe programming languages. More specifically, I work on runtime type analysis and generation of type-safe object code.

Many programming applications like garbage collection, pickling, dynamic linking, etc, use type information at runtime. Implementing these applications in a type-safe language requires language support for runtime type analysis. Runtime type analysis in a type-safe framework was first studied by Harper and Morrisett in their paper titled "Compiling Polymorphism Using Intensional Type Analysis". Their paper deals with the analysis of inductively defined types, but fails to handle quantified types. In a recent paper we show how to analyze arbitrary source language types.

I also believe that type-safety can be used as a practical basis for generating certified code. Therefore, I am working on propagating types through all phases of compilation. The goal is to generate type correct object code that also supports runtime type analysis. I intend to use a type and kind erasure framework for this. In a recent paper we show how to support type analysis over arbitrary types in a type erasure framework.

The type-safety of a programming system relies crucially on the type-safety of runtime services. I am also interested in the type-safe implementation of these services. In a recent paper we show how to type-check a copying garbage collector using intensional type analysis.

I work in the FLINT group and my advisor is Prof. Zhong Shao. I mostly use the Standard ML programming language and the FLINT/ML compiler. We also collaborate with researchers at Princeton University and Bell Labs on the DARPA/PCC and SML/NJ projects.

Publications