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. I am particularly interested in both the design and semantics of next-generation programming languages, which I believe will be rooted in functional programming but will include support for a mix of different programming paradigms.

On the design side, I have focused on extending the ML module system (one of the most advanced module system designs) with a variety of features, including higher-order modules, type classes, and recursive modules. The pinnacle of this work is the design of MixML, a type system I co-developed with Andreas Rossberg, which seamlessly synthesizes the essential aspects of ML modules and Bracha-style "mixin" modules. This remains the single piece of work I am most proud of.

On the semantics side, I have focused on developing effective techniques for reasoning about program equivalence in modern languages. Program equivalence is an important problem, with applications to program verification, representation independence, and compiler correctness, among other things. It is also an old, hard problem: until recently, effective models of program equivalence were only available for fairly restricted languages. Nevertheless, thanks to a few recent semantic developments---most importantly, step-indexed models, biorthogonality (TT-closure), and advances in Kripke logical relations---my collaborators and I have managed to develop relational reasoning techniques for modern languages that support polymorphism, general recursive types, higher-order mutable state, dynamic type analysis, exceptions, first-class continuations, and more.

Please see my most recent research statement for further details.

Professional Activities

Program chair:
- TLDI 2011
- ML 2007
Program committee member:
- 2011: POPL, TLDI
- 2010: MLPA, FOOL
- 2009: MFPS, MLPA
- 2008: ICFP
- 2007: FOOL/WOOD, Haskell, ML
- 2006: ML
Invited participant, Dagstuhl Seminar on Modelling, Controlling and Reasoning About State (Aug/Sep 2010)
Workshops co-chair, ICFP 2010 and ICFP 2011
Moderator, TYPES and TYPES/announce mailing lists (April 2009--present)
External review committee member, PLDI 2009
Invited speaker, MFPS 2008
Steering committee member, Workshop on ML (2008--present)
Invited participant, IFIP WG2.8 Meeting (July 2007)

Research Group Members

Current:

Scott Kilpatrick, student (since Aug. 2010)
Georg Neis, student (since Nov. 2008)
Beta Ziliani, student (since Jan. 2010)

Future:

Chung-Kil Hur, postdoc (starting Oct. 2010)

Past:

Andreas Rossberg, postdoc (Aug. 2007 -- Jan. 2010, now at Google Munich)

External Collaborators

Amal Ahmed (Indiana University)
Lars Birkedal (IT University of Copenhagen)
Matthias Blume (Google Chicago)
Manuel Chakravarty (University of New South Wales)
Karl Crary (Carnegie Mellon University)
Bob Harper (Carnegie Mellon University)
Gabriele Keller (University of New South Wales)
Claudio Russo (Microsoft Research Cambridge)

Recent Submissions

A Kripke Logical Relation Between ML and Assembly.
Chung-Kil Hur and Derek Dreyer.
Submitted for publication, July 2010.
Draft: (abstract, paper, appendix)

Non-Parametric Parametricity.
Georg Neis, Derek Dreyer, and Andreas Rossberg.
Submitted for publication, April 2010.
This is a revised and expanded version of our ICFP 2009 paper.
Draft of Journal Version: (abstract, paper)

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
Submitted for publication, January 2010.
This is a revised, corrected, and expanded version of our LICS 2009 paper.
Draft of Journal Version: (abstract, paper)

Publications

The Impact of Higher-Order State and Control Effects on Local Relational Reasoning.
Derek Dreyer, Georg Neis, and Lars Birkedal.
In 2010 ACM SIGPLAN International Conference on Functional Programming (ICFP 2010).
Conference Version: (abstract, paper, appendix)

F-ing Modules.
Andreas Rossberg, Claudio V. Russo, and Derek Dreyer.
In 2010 ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2010).
Workshop Version: (abstract, paper, Coq script)

A Relational Modal Logic for Higher-Order Stateful ADTs.
Derek Dreyer, Georg Neis, Andreas Rossberg, and Lars Birkedal.
In 2010 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010).
Conference Version: (abstract, paper, appendix) Talk Slides: (pdf)

Non-Parametric Parametricity.
Georg Neis, Derek Dreyer, and Andreas Rossberg.
In 2009 ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
Conference Version: (abstract, paper)
Long Version: (Georg Neis's master's thesis)

Logical Step-Indexed Logical Relations.
Derek Dreyer, Amal Ahmed, and Lars Birkedal.
In 2009 IEEE Symposium on Logic in Computer Science (LICS 2009).
Conference Version + Appendix: (abstract, paper) Talk Slides: (pdf)
This paper suffers from a non-negligible (if ultimately minor) technical flaw.
See our LMCS submission above for a revised, corrected, and expanded version.

State-Dependent Representation Independence.
Amal Ahmed, Derek Dreyer, and Andreas Rossberg.
In 2009 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2009).
Conference Version: (abstract, paper, appendix)

Mixin' Up the ML Module System.
Derek Dreyer and Andreas Rossberg.
In 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP 2008).
Conference Version: (abstract, pdf) Talk Slides: (pdf)
Expanded Version: (pdf, project website)

Mechanizing the Metatheory of a Language With Linear Resources and Context Effects.
Daniel K. Lee, Derek Dreyer, and Andreas Rossberg.
In 2008 ACM SIGPLAN Informal Workshop on Mechanizing Metatheory (WMM 2008).
Abstract: (pdf) Talk Slides: (pdf)

A Type System for Recursive Modules.
Derek Dreyer.
In 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP 2007).
Conference Version: (abstract, pdf)
University of Chicago Comp. Sci. Dept. Technical Report TR-2007-10, July 2007.
Technical Report: (pdf)

Recursive Type Generativity.
Derek Dreyer.
Journal of Functional Programming (JFP). 17(4&5), 433--471, July & September 2007.
Special issue devoted to selected papers from ICFP 2005.
Journal Version: (abstract, paper)
Principal Type Schemes for Modular Programs.
Derek Dreyer and Matthias Blume.
In 2007 European Symposium on Programming (ESOP 2007).
Conference Version: (abstract, pdf) Talk Slides: (ppt)
University of Chicago Comp. Sci. Dept. Technical Report TR-2007-02, January 2007.
Supersedes TR-2006-08, October 2006. Technical Report: (pdf)

Modular Type Classes.
Derek Dreyer, Robert Harper, and Manuel M.T. Chakravarty.
In 2007 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007).
Conference Version: (abstract, pdf) Talk Slides: (ppt)
University of Chicago Comp. Sci. Dept. Technical Report TR-2006-09, October 2006.
Supersedes TR-2006-03, April 2006. Technical Report: (pdf)

Recursive Type Generativity.
Derek Dreyer.
In 2005 ACM SIGPLAN International Conference on Functional Programming (ICFP 2005).
Conference Version: (abstract, paper) Talk Slides: (ppt)
This paper is superseded by the JFP version cited above.

A Type System for Well-Founded Recursion.
Derek Dreyer.
In 2004 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004).
Conference Version: (abstract, pdf) Talk Slides: (ppt) Technical Report: (pdf)

A Type System for Higher-Order Modules.
Derek Dreyer, Karl Crary, and Robert Harper.
In 2003 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2003).
Conference Version: (abstract, pdf) Talk Slides: (ppt) Technical Report: (pdf)

Typed Compilation of Recursive Datatypes.
Joseph C. Vanderwaart, Derek Dreyer, Leaf Petersen, Karl Crary, Robert Harper, and Perry Cheng.
In 2003 ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2003).
Conference Version: (abstract, pdf) Talk Slides: (ppt) Technical Report: (pdf)

Two Heuristics for the Euclidean Steiner Tree Problem.
Derek R. Dreyer and Michael L. Overton.
Journal of Global Optimization, 13: 95-106, 1998.
Journal Version: (abstract, pdf)

Ph.D. Thesis

Understanding and Evolving the ML Module System.
Derek Dreyer.
Ph.D. Thesis, CMU Technical Report CMU-CS-05-131, May 2005.
Technical Report: (abstract, pdf)

Other Technical Reports and Drafts

Practical Type Theory for Recursive Modules.
Derek Dreyer.
University of Chicago Comp. Sci. Dept. Technical Report TR-2006-07, August 2006.
Technical Report: (abstract, pdf)

Toward a Practical Type Theory for Recursive Modules.
Derek R. Dreyer, Robert Harper, and Karl Crary.
CMU Technical Report CMU-CS-01-112, March 2001.
Technical Report: (abstract, pdf)

Derek Dreyer

Last modified: Fri Aug 13 00:09:59 CEST 2010