|
|
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
- High-Level Optimization of MATLAB Programs
- G, a language for generic programming. Planned extensions:
- Meta-programming
- Optimization
- Existential types
- Gradual typing is a type system I developed 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.
- 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.
- C++. I am working on the C++ Standards
Committee to improve support for generic programming in C++. We describe
our proposal in the paper Concepts
for C++0X.
- Datalog is a Database/logic programming language. I'm
developing a fancy type system for it.
Graduate Students
- Joe Angell is working on gradual typing for Python
Past Research
|
|
