Research

My CV and most of my publications are available on-line.

My research usually involves the theory or implementation of programming languages. I am particularly interested in type systems for functional and object-based languages.

Recently I've started the Observationally Cooperative Multithreading (OCM) project with Prof. Melissa O'Neill and a sizable number of undergraduate students. In traditional Cooperative Multithreading (CM), one thread runs at a time, and each thread runs until it explicitly yields the processor to the next thread. This permits a very simple and efficient programming model, because the lack of unexpected preemption means that that locks and the problems that go with them (not enough locks = race conditions, too many locks or locks acquired in the wrong order = deadlock) can be avoided.

The goal of OCM is to port the CM model to a multiprocessor. When threads are non-interacting, we run them simultanously without any change in behavior except for improved speed. Preliminary experiments with modified Lua interpreters (an optimistic-concurrency implementation using Software Transactional Memory and a pessimistic implementation internally using locks) are very encouraging. We have an unpublished manuscript describing Observationally Cooperative Multithreading in more detail.

Previously I worked on a translator that turns constructive-mathematics specifications into interface code for programmers. The system answers questions like, "What would a programmer need to implement in order to get a complete and correct implementation of the mathematical real numbers [or a compact metric space, or a space of smooth functions, ...]?" From an educational perspective, it also provides explanations (in terms a programmer can understand) of the non-classical distinctions that arise in constructive mathematics. For example, one can explain the difference between a finite set and a set that is not infinite, and why there is a "size" function only for the former.

I have also worked on types for object-based languages (languages that permit adding new fields or methods to individual objects at run-time) and on type checking algorithms for recursively-defined types.