David Walker Computer Science Dept. Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, P.A. 15213-3891 Email: dpw@cs.cmu.edu Office: 7112 Wean Hall Phone: (412) 268-6714

Future:

• Starting February 2002, I will be an assistant professor in the Computer Science Department at Princeton University. If you have questions about the future of programming languages at Princeton, please let me know -- it is sure to be exciting.
• I will be unavailable between November 13th and December 9th, 2001. I will attempt to process email for that time period during the week following my return. In case of personal emergencies, please contact my parents in Toronto at (416) 481-9145.

Research:

I study the design, implementation and theory of programming languages. I am particularly interested in finding new ways to use type systems and logics to help programmers write more reliable and secure code.

A significant portion of my tenure as a Ph.D. student at Cornell University was spent working with Greg Morrisett and others on the design and implemention of a type system for the Intel Pentium processor called TAL. Like Java applets, TAL programs (ie: binaries containing Pentium machine code and associated typing annotations) may be downloaded by untrusting clients and checked for safety. TAL has a firm theoretical foundation and a variety of practical tools that allow us to compile programs written in a safe variant of C and to verify the output.

One of the main challenges in the design of strongly typed low-level languages is the development of a safe, yet flexible memory model. Safe languages normally present a highly simplified and restrictive memory model to the programmer and as a result, programmers (or compilers, if their output is a type safe language such as TAL or JVM bytecode) cannot implement their own optimized, application-specific memory management. In my thesis, I address this problem by developing a family of type systems that control aliasing and check the safety of programs containing explicit initialization, deallocation and reuse of memory. The TAL type checker uses one of these type systems to reason about aliasing in assembly language programs.

I am now a post-doc at Carnegie Mellon University, working with the FOX Project and TILT groups on advanced programming language technology for systems software. With Iliano Cervesato and Frank Pfenning, I am investigating new ways to use formal logic, logical frameworks and programming language technology to aid in the specification of security protocols and verification of their implementations. With Bob Harper and Kevin Watkins, I am investigating modular and compositional reasoning about state. I also continue to collaborate with Dan Grossman, Greg Morrisett and Trevor Jim at Cornell on memory management issues for a new type-safe variant of C called Cyclone.

Research Publications and Slides from Selected Talks

Curriculum Vitae (Last Updated December 2000)

Research Statement

Teaching Statement

Professional Activities:

• Program committee, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM), Portland, Oregon, Jan. 14-15, 2002. In association with the Symposium on Principles of Programming Languages (POPL '02). Please submit a paper!
• ACM state-of-the-art summer school on Foundations of Internet Security, Duszniki Zdrój, Poland, postponed due to the tragic events of September, 2001. I will be giving a series of lectures on type systems for safe mobile code with a focus on the theoretical development of Typed Assembly Language. For a preview, see my slides on TAL. They represent the broadest description of what goes into Typed Assembly Language that is available at an introductory level. Other topics taught at the school range from Java security to cryptography to formal analysis of authentication protocols to intrusion detection.

Teaching:

• Foundations of Language-based Security. Spring, 2002. Princeton.
• Invited lectures given in John Reynolds course on reasoning about low-level programs. March 2001.
• CS 113: C Programming(Instructor, Fall '97)
• Cornell Computer Science Outstanding TA Award(May, '97)
• CS 501: Software Engineering(Teaching Assistant, Fall '96)
• CS 211: Computers and Programming(Teaching Assistant, Fall '95, Spring '96)

Fun I am a firm believer everyone should do a little whitewater kayaking every now and then. Everything I've learned about this sport and about surviving in the outdoors in general, I learned at Kandalore. My other outdoor passion is canoe tripping. Two summers ago I did a month-long trip down the Mistassibi and when I was a teenager, I did the Missinaibi from Dog Lake to Moosonee. In the summer of '98 I got back there to do a 10-day trip along the section from Missinaibi Lake to Mattice. I've also traveled the Dumoine, Spanish, Magnetewan, and Petawawa Rivers, among others in Quebec and Ontario. I'd love to get out to the Nahanni, Copper Mine, or (more realistically) the Moisie but it is getting harder and harder to find the time ... When I'm not exploring the unknown wilds (ie: most of the time), I satisfy myself while a little old-fashioned shinny (hockey), the occasional trip to the ski slopes, or a little bridge. I've also picked ultimate (frisbee) recently.

Quote of the Month (changed semi-annually) It's hockey season again: Go Leafs go!