Daniel Lee

Doherty Hall, 4301F
Phone: (412) 268-2039

Graduate student in the Computer Science Department at Carnegie Mellon University since Fall 2005. My advisors are Bob Harper and Karl Crary. I also benefit from the mentorship of Peter Lee. My general interests include type systems, programming languages, and certifying compilation. My current work involves mechanizing a specification and type-safety proof for Standard ML.

I was supported by a National Science Foundation Graduate Research Fellowship from Fall 2005 to Spring 2008.

Bachelor of Arts, double major in Computer Science and Economics from Cornell University, May 2005.

Research Projects, Past and Present

These are various research projects I've worked on and the people I worked with.

• Mechanizing the Metatheory of Standard ML
  • Karl Crary
  • Robert Harper
• Mechanizing the Metatheory of RTG (Summer 08)
  • Derek Dreyer
  • Andreas Rossberg
  • Max Planck Institute for Software Systems
• Typesafe IA Project (Summer 06)
  • Neal Glew
  • Kamal Aboul-Hosn
  • Leaf Petersen
  • Intel Programming Systems Lab
• McCabe Cyclomatic Complexity and other software metrics for BEAM, a source analysis tool. (Summer 05)
  • Siddhartha Chatterjee
  • Greg Russell
  • Dan Brand
  • IBM T.J. Watson Research Center
• Polyglot, a compiler front end framework for building Java language extensions.
  J0, a variant of Java designed for novice programmers written with Polyglot.
  • Andrew Myers
• Avrora, a framework for analysis and event-based simulation of AVR microcontroller programs. (Summer 04)
  • Ben Titzer
  • Jens Palsberg
  • UCLA Compilers Group
• Cyclone, a type-safe dialect of the C programming language.
  • Greg Morrisett

Publications

• Daniel K. Lee, Derek Dreyer, and Andreas Rossberg. Mechanizing the Metatheory of a Language With Linear Resources and Context Effects. (Long Abstract) In the web proceedings of the Third Informal Workshop on Mechanizing Metatheory, Victoria, British Columbia, September 2008.
• Daniel K. Lee, Karl Crary, and Robert Harper. Towards a Mechanized Metatheory of Standard ML. In Proceedings of the 2007 Symposium on the Principles of Programming Languages, January 2007. BibTex Long version. CMU Technical Report CMU-CS-06-138. Twelf Source Code.
• Daniel K. Lee, Karl Crary, and Robert Harper. Mechanizing the Metatheory of Standard ML. (Long Abstract) In the web proceedings of the First Informal Workshop on Mechanizing Metatheory, Portland, Oregon, September 2006.
• Ben L. Titzer, Daniel K. Lee, and Jens Palsberg. Avrora: Scalable Sensor Network Simulation with Exact Timing. In Proceedings of IPSN'05, Fourth International Conference on Information Processing in Sensor Networks, pages 477-482, Los Angeles, California, April 2005. BibTex

Research/Intellectual Interests

To some degree or another, I am interested in the following:

• The SML programming language, its variants, and its future
• Mechanized metatheory for realistic programming languages
• Functional programming
• Cool type systems
• Singleton types
• Dependent types
• Typed assembly and intermediate languages
• Certified code/certifying compilation
• The implementation of operating systems with modern, type-safe programming languages
• Event-based simulation models for embedded sensor networks
• Game theory

Teaching

• Spring 2008: Teaching Assistant 15-312 Principles of Programming Languages
• Spring 2006: Teaching Assistant 15-317 Constructive Logic

Coursework

• FA 2007: 15-819F Languages and Logics for Security
• FA 2007: 15-780* Graduate Artificial Intelligence
• SP 2007: 15-818A3 Introduction to Separation Logic
• SP 2007: 15-818A4 Current Research on Separation Logic
• SP 2007: 15-744* Computer Networks
• FA 2006: 15-819K Logic Programming
• FA 2006: 15-855* Complexity Theory
• SP 2006: 15-745* Optmizing Compilers. Final Project
• FA 2005: 15-814* Type Systems
• FA 2005: 15-819H HOT Compilation

Twelf Elf Rotation

If you want to join the rotation, contact me or just send an e-mail to the Twelf Elf address. Membership is not limited to people at CMU. Some fluency with Twelf is obviously helpful.

Worthwhile Wikis

• Wikipedia
• successor ML
• Twelf Wiki

Random Bits

My homepage has the uncommon feature of including "Things" Lists

Because I couldn't find one, I decided to start compiling a list of left-handed computer scientists.

Call me Dan or Daniel, and I'll eventually guess that you are talking to me. Call me D, and I'll assume you are talking to me.

Every now and then, I take a moment and remind myself that I am a high school drop-out.

I am a coffee elf.

Are you "Server OK" today?

Some computer scientists like to see where they end up on this ranking of first initial/last name by citations. The relative stupidity of the algorithm that compiles this information produces a few amusing results. Given the fact that "D. Lee" is not terribly unique and there must be some terribly prolific "D. Lee"s out there, I rank around 110 out of 10,000, through virtually no influence of my own. That's way above thousands of very smart people (and a handful of non-existent ones)! As of August 2006, other amusing entries include "P. Thesis" at 601, "M. Interface" at 1247, "D. Networks" at 3532, "A. Computer" at 5902, "I. Processing" at 6827, "A. Network" at 8171, "M. Thesis" at 8301, "L. Http" at 8595, "P. Dissertation" at 8603, and "S. Verlag" at 9470.

This site is still a work in progress. I imagine it will continue to be for the next n years.

For lack of a tool that annoyed me less, I have developed this site with various variants of the Emacs text editor.