My research interests are in the areas of programming languages and software engineering with applications in the computational sciences. In particular, I am interested in language support for high-performance software libraries and domain specific languages. My research includes work in type systems, optimizing compilers, program logics, and language facilities for program generation.

Current Projects

• Gradual typing is a type system I developed with Walid Taha that allows a program to be dynamically typed in parts and statically typed in other parts. The programmer controls which parts are dynamic/statically checked by either leaving out type annotations on function parameters, or by putting in the type annotations.
  • Gradual typing for functional languages. In Scheme and Functional Programming Workshop, September 2006. [pdf] [bibtex]
  • Gradual Typing for Objects. In ECOOP 2007: European Conference on Object-Oriented Programming, Berlin, Germany, July 2007.
    [pdf] [bibtex]
  • Gradual Typing with Unification-based Inference. In the Dynamic Languages Symposium 2008. [pdf][bib][implementation]
  • Exploring the Design Space of Higher-Order Casts. In ESOP: European Symposium on Programming, York, United Kingdom, March 2009.
    [pdf] [bibtex]
  • Threesomes, With and Without Blame. In the First International Workshop on Script to Program Evolution (STOP 2009) [pdf]
  • Threesomes, With and Without Blame. Accepted for POPL 2010. [pdf] Supersedes the STOP 2009 paper.
• Build To Order BLAS (project webpage)
  • Automating the Generation of Composed Linear Algebra Kernels. In SC09: the International Conference on High Performance Computing, Networking, Storage, and Analysis. November, 2009. [pdf] [bib] [DOI]
  • Generating Empirically Optimized Composed Matrix Kernels from MATLAB Prototypes. In International Conference on Computational Science 2009.
  • Build to Order Linear Algebra Kernels [pdf][bib]. In the Workshop on Performance Optimization of High-level Languages and Libraries (POHLL'08).
• G, a language for generic programming. Planned extensions:
  • Meta-programming
  • Optimization
  • Existential types

Past Research

• C++ Concepts. I worked on the C++ Standards Committee to improve support for generic programming in C++. We described our proposal in the paper Concepts for C++0X.
• Concoqtion is an extension of MetaOCaml with indexed types (a kind of dependent type), where the indexes are propositions expressed in the Coq language. This extension makes the type system much more expressive. The extended type system uses the Coq theorem prover during type checking, and the programmer may include proofs written in Coq. This work is in collaboration with Walid Taha at Rice University.
• The topic of my Ph.D. thesis is a new programming language, named G, for generic programming. The paper Essential Language Support for Generic Programming at PLDI'05 describes the core of the language and the paper Language Requirements for Large-Scale Generic Libraries at GPCE'05 gives an overview of the full language and describes a reimplementation of the STL in G.
• I designed and implemented the Boost Graph Library with Andrew Lumsdaine and Lie-Quan Lee, and wrote the book The Boost Graph Library: User Guide and Reference.
• My master's thesis applied generic programming techniques to the constrution of Matrix Template Library, a library for numerical linear algebra. I also helped with the design and implementation of the Iterative Template Library.