My Research

I received my Ph.D. in Computer Science from Carnegie Mellon University in May 2005.
From January 2005 to December 2007, I was a research assistant professor (3-year postdoc) at the Toyota Technological Institute at Chicago (TTI-C).
Since January 2008, I am an independent researcher (tenure-track faculty) at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany, heading the Type Systems and Functional Programming group.

Curriculum Vitae Research Activities Professional Activities Collaborators Publications

Research Activities

My primary research interests are in functional programming languages and their foundations in type theory. My work to date has focused on ML, one of the most widely used HOT (higher-order, typed) functional languages. In my thesis work, I developed a unified way of understanding the ML module system that clarifies the relationships between existing dialects of ML. I also studied the problem of extending ML with support for recursive modules, and implemented an experimental recursive module extension in the TILT compiler, developed at CMU.
After moving to TTI-Chicago, I continued my thesis work on evolving the ML module system. I developed a type system for recursive modules that is the first to solve a critical problem involving the interaction of recursion and data abstraction known as the double vision problem. In other work with Bob Harper and Manuel Chakravarty, I showed how to extend ML with support for overloading and ad hoc polymorphism through Haskell-style type classes. This work exposes deep connections between ML modules and Haskell type classes, resulting in a unifying account of the two features that encourages modularity and avoids redundancy of mechanism. In the process of extending ML with type classes, I discovered an oversight in the Definition of Standard ML, namely that the classic principal types property of core ML does not generalize properly in the presence of modules. Subsequently, in work with Matthias Blume, I showed how to regain principal types for full ML by exploiting techniques developed in my (superficially unrelated) study of recursive modules.
After accepting a tenure-track position at MPI-SWS, I was fortunate to hire Andreas Rossberg as a postdoc in my Type Systems and Functional Programming research group. Andreas and I have developed a novel module system design that addresses one of the key remaining problems with recursive modules, namely separate compilation. This design seamlessly integrates elements of both traditional ML module systems and Bracha-style mixin modules, resulting in a clean, elegant, and minimalist account of the ML module system that unifies a variety of superficially distinct features. A prototype implementation is available here.

Professional Activities

Collaborators

Recent Submissions

Publications

Ph.D. Thesis

Other Technical Reports and Drafts

Derek Dreyer

Last modified: Sat Mar 01 16:54:45 W. Europe Standard Time 2008