Derek Dreyer → Research

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.

From January 2005 to December 2007, I was a research assistant professor (3-year postdoc) at the Toyota Technological Institute at Chicago (TTI-C).

Before that, I studied type theory with Bob Harper and Karl Crary at Carnegie Mellon University, receiving my Ph.D. in Computer Science in May 2005.

Curriculum Vitae Research Activities Professional Activities Research Group Members External 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 and generalizes a variety of superficially distinct features. A prototype implementation is available here.

More recently, I've been working on reasoning about the semantics of modules, a topic that is of crucial importance as module languages grow more complex. As a starting point, in work with Amal Ahmed and Andreas Rossberg, I've set out to prove some simple results about how type generativity allows one to tie the (relational) interpretation of an abstract type to local state. These results, while simple to state, have been devilishly hard to prove, due to the subtle interaction of higher-order, functional and imperative features that are involved. Our technique involves the use of step-indexed logical relations. While this is a powerful technique, it also results in step-index (natural number) arithmetic spreading like moss over otherwise-readable proofs. So, more recently, in work with Amal Ahmed and Lars Birkedal, I've developed a logic for reasoning about step-indexed logical relations in a more abstract way that doesn't mention steps.

Professional Activities

Research Group Members

Current: Former:

External Collaborators

Recent Submissions

Publications

Ph.D. Thesis

Other Technical Reports and Drafts

Derek Dreyer

Last modified: Sat Feb 6 23:41:51 CET 2010