I study the theory, design, and implementation of modern programming languages. I am particularly interested in finding new ways to use logic, type theory and static analysis to help programmers write efficient, yet secure and reliable code. Specific research topics include: Certifying compilation, typed intermediate languages, typed assembly language and proof-carrying code; logic and type systems for reasoning about safety properties, memory management, aliasing and security; applications of programming language technology to the design and implementation of systems software.

• Type-Directed Certifying Compilation. With Greg Morrisett and others at Cornell University, I studied type-directed compilation and type systems for low-level languages. One of our main contributions was the design and implementation of the first typed assembly language (TAL). TAL programs are composed of Intel Pentium code and a variety of typing annotations. Like Java Virtual Machine applets, TAL programs can be distributed over the Internet and checked for safety by untrusting hosts. See http://www.cs.cornell.edu/talc for the latest release of our TAL type checker and compilers.
• Typed Memory Management. For my thesis, I explored type systems for reasoning about higher-order imperative programs that explicitly allocate and deallocate memory. One important contribution of my thesis is a novel type system for region-based memory management. My work on type-theoretic mechanisms for reasoning about aliasing is used to verify the safety of TAL programs.

• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In Transactions on Systems and Programming Languages, 21(3):528-569, May 1999.
• David Walker, Karl Crary and Greg Morrisett. Typed Memory Management Via Static Capabilities. Transactions on Systems and Programming Languages, to appear. Accepted May 2000.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based Typed Assembly Language. Submitted to the Journal of Functional Programming.

• David Walker and Kevin Watkins. On Regions and Linear Types. In the Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, London, Jan. 2001.
• David Walker and Greg Morrisett. Alias Types for Recursive Data Structures. In the Workshop on Types in Compilation, Montreal, Sept. 2000.
• Fred Smith, David Walker and Greg Morrisett. Alias Types. In the European Symposium on Programming, Berlin, March 2000. Published in Gert Smolka, editor, Lecture Notes in Computer Science, volume 1782, pages 366-381.
• David Walker. A Type System for Expressive Security Policies. In the Twenty-Seventh ACM SIGPLAN Symposium on Principles of Programming Languages. Boston, January 2000. A previous version of this paper appeared in the FLOC'99 Workshop on Run-time Result Verification, Trento, Italy, July 1999.
• Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A Realistic Typed Assembly Language. In the ACM SIGPLAN Workshop on Compiler Support for System Software, INRIA Research Report 0228, pages 25-35, Atlanta, May 1999.
• Karl Crary, David Walker, and Greg Morrisett. Typed Memory Management in a Calculus of Capabilities. In the Twenty-Sixth ACM Symposium on Principles of Programming Languages , pages 262-275, San Antonio, Jan. 1999.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-Based Typed Assembly Language. In the 1998 Workshop on Types in Compilation, Kyoto, Japan. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer, March 1998.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In the Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85-97, San Diego, Jan. 1998.

• Alias Types. Invited talk, Carnegie Mellon Computer Science Department Principles of Programming Languages Seminar, Pittsburgh, April 25.
• Secure Certifying Compilation. Invited talk, IBM T. J. Watson, New York, April 12, 2000.
• A Type System for Expressive Security Policies at the Symposium on Principles of Programming Languages in Boston, Jan. 20, 2000.
• Typed Memory Memory Management in a Calculus of Capabilities at the Symposium on Principles of Programming Languages in San Antonio, Jan. 21, 1999.
• Stack-Based Typed Assembly Language at the 1998 Workshop on Types in Compilation in Kyoto, Japan, March 26, 1998.

• Instructor: Introductory C Programming (100 level). Fall ‘97.
• Cornell Computer Science Outstanding TA Award. May ‘96.
• Teaching Assistant: Software Engineering (500 level). Fall ’96.
• Teaching Assistant: Computers and Programming (200 level). Spring ’96 Fall ’95.

• Program committee, Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM), Jan. 2002.
• Referee for workshops, conferences and journals on programming languages
  • Including the Journal of Functional Programming, and ACM SIGPLAN Conferences and Workshops on Functional Programming (ICFP), Principles of Programming Languages (POPL), Foundations of Object-Oriented Languages (FOOL), and Programming Language Design and Implementation (PLDI).

• Cornell University: Ph.D. in Computer Science, Aug 95 - Jan 2001.
  • Thesis: Typed Memory Management, Jan 2001
  • Thesis Committee Chair: Greg Morrisett
  • Awarded Masters of Science, May 1999
  • GPA: 4.0, Minor field: English Literature
• Queen’s University, Kingston, ON: B.Sc. (Hon.) ’95, Computer Science
  • Prince of Wales Prize, Honorable Mention ’95 (2^nd highest standing in faculty of Arts and Science, Queen’s University)
  • R. W. Leonard Penultimate Year Scholarship ‘94 (highest standing through 3 years of B.Sc., Queen’s University)

• Postdoctoral Fellow, Carnegie Mellon University (September 2000 - present)
  • FOX Project: Advanced Programming Language Technology for Systems Software
  • Colleagues: Bob Harper, Peter Lee, Frank Pfenning
• Research Assistant, Cornell University(Spring 97 - Summer 2000)
  • Adviser: Greg Morrisett
• Teaching Assistant, Cornell University (Fall 95 - Fall 97)
• Kandalore Camp (Summer 91-93, 95, 96)
  • Organized and led wilderness whitewater canoe trips of up to four weeks in duration.
• Research Assistant, University of Toronto (Summer 94)
  • Studied and evaluated network protocols under Mart Molle.
• Kandalore Outdoor Education Center (May-June 92, 93)
  • Taught leadership and communication skills to groups of school childern aged 11-15.

• Greg Morrisett, Assistant Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  jgm@cs.cornell.edu
• Dexter Kozen, Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  kozen@cs.cornell.edu
• Frank Pfenning, Associate Professor
  Computer Science Dept., Carnegie Mellon University
  5000 Forbes Avenue
  Pittsburgh, PA 15213
  fp@cs.cmu.edu
• Bob Constable, Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  rc@cs.cornell.edu