Tremen Park, Ithaca, NY

David Walker

Computer Science Dept.
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, P.A. 15213-3891

Office: 7112 Wean Hall
Phone: (412) 268-6714



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:


  • 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.
Dave 'yaking

Mistassibi River, North-Central Quebec Quote of the Month (changed semi-annually)
It's hockey season again: Go Leafs go!