David Walker
Department of Computer Science
Princeton University
35 Olden St.
Princeton, NJ 08540
(609) 258-7654
dpw@cs.princeton.edu
Research Focus
I study the theory, design, and implementation of modern programming languages. Specific research topics include: Program logics and type systems; Ad hoc data processing; Reasoning about software in the presence of transient hardware faults; Certifying compilation; Language-based security.
Books and Journal Articles
The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum, David Walker. Submitted for journal publication. Generated December 2006.
A Type-Theoretic Interpretation of Pointcuts and
Advice. Jay Ligatti, David Walker and Steve Zdancewic. Science of Computer
Programming. Volume 63, Issue 3, pp 240-266. December 2006.
AspectML: A Polymorphic Aspect-oriented Functional Programming Language.
Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich. Submitted
for journal publication. Generated March 2006.
Substructural Type Systems. David Walker. Chapter 1 of Advanced Topics in Types and Programming Languages. Benjamin Pierce, ed. January 2005.
Edit Automata: Enforcement Mechanisms for Run-time Security Policies. Jay Ligatti, Lujo Bauer and David Walker. International Journal of Information Security, Volume 4, Number 2, pp. 2-16, February 2005. ISSN: 1615-5262, Springer-Verlag.
Stack-based Typed Assembly Language. Greg Morrisett, Karl Crary, Neal Glew, and David Walker. In the Journal of Functional Programming, 12(1):43-88, January 2002.
Typed Memory Management Via Static Capabilities. David Walker, Karl Crary and Greg Morrisett. In Transactions on Systems and Programming Languages, 22(4):701-771, July 2000.
From System F to Typed Assembly Language. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. In Transactions on Systems and Programming Languages, 21(3):528-569, May 1999.
Refereed Conference & Workshop Papers; Selected Technical Reports
PADS/ML: A Functional Data Description Language. Yitzhak Mandelbaum, Kathleen Fisher, David Walker, Mary Fernandez, and Artem Gleyzer. ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages. January 2007.
Expressing
Heap-shape Contracts in Linear Logic. Frances Spalding, Limin Jia and David
Walker. ACM SIGPLAN-SIGSOFT International Conference on Generative Programming
and Component Engineering. October 2006.
Static Typing for a Faulty Lambda Calculus. David Walker, Lester Mackey, Jay
Ligatti, George Reis, and David August. ACM SIGPLAN International Conference on
Functional Programming. September 2006.
Mechanized Metatheory for User-Defined Type Extensions. Daniel Marino, Brian
Chin, Todd Millstein, Gang Tan, Robert J. Simmons and David Walker. ACM SIGPLAN
Workshop on Mechanizing Metatheory. September 2006.
PADS/ML: A Functional Data Description Language. Yitzhak Mandelbaum, Kathleen Fisher, David Walker, Mary Fernandez, and Artem Gleyzer. Princeton University Technical Report TR-761-06. July, 2006.
Linear Logic, Heap-shape Patterns and Imperative Programming. Limin Jia and
David Walker. Princeton University Technical Report TR-762-06. July, 2006.
PADS: An End-to-end System for Processing Ad Hoc Data. Mark Daly, Mary
Fernandez, Kathleen Fisher, Robert Gruber, Yitzhak Mandelbaum, David Walker and
Xuan Zheng. ACM SIGMOD demo. June 2006.
ILC: A Foundation for Automated Reasoning about Pointer Programs.
Limin Jia and David Walker. European Symposium on Programming Languages. In
Programming Languages and Systems, LNCS 3924, pp 131-145, Peter Sestoft editor.
March 2006.
Making Extensibility of System Software Practical with the C4 Toolkit. Marco
Yuen, Marc E. Fiuczynski, Robert Grimm, Yvonne Coady and David Walker. Workshop
on Software Engineering Properties of Languages and Aspect Technologies. March
2006.
The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum
and David Walker. ACM SIGPLAN-SIGACT Symposium on Principles of Programming
languages. January 2006.
Harmless Advice. Daniel S. Dantas and David Walker. ACM SIGPLAN-SIGACT
Symposium on Principles of Programming languages. January 2006.
LaunchPADS: A System for Processing Ad Hoc Data. Mark Daly, Mary Fernandez,
Kathleen Fisher, Yitzhak Mandelbaum and David Walker. Demo Paper in PLAN-X 06:
Programming Language Technologies for XML. January 2006.
PolyAML: A Polymorphic Aspect-oriented Functional Programmming Language. Daniel S. Dantas, David Walker, Geoffrey Washburn and Stephanie Weirich. ACM International Conference on Functional Programming. September 2005.
PADS/T: A Language for Describing and Transforming Ad Hoc Data. Mary Fernandez, Kathleen Fisher, Yitzhak Mandelbaum and David Walker. Princeton University Technical Report TR-736-05. September, 2005.
Composing Security Policies in Polymer. Lujo Bauer, Jay Ligatti and David Walker. ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2005.
Certifying Compilation for a Language with Stack Allocation. Limin Jia, Frances Spalding, David Walker and Neal Glew. IEEE Symposium on Logic in Computer Science. June 2005.
Patch(1) Considered Harmful. Marc E. Fiuczynski, Robert Grimm, Yvonne Coady and David Walker. Workshop on Hot Topics in Operating Systems. June, 2005.
Refined Proof Theory for Reasoning About Separation. Limin Jia and David Walker. IEEE Symposium on Logic in Computer Science, short paper. June 2005.
Harmless Advice. Daniel S. Dantas and David Walker. In Foundations of Object-Oriented Languages, January 2005.
Dynamic Typing with Dependent Types (extended abstract). Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. In the 3rd IFIP International Conference on Theoretical Computer Science, August, 2004.
Specifying Properties of Concurrent Computations in CLF. Kevin Watkins, Iliano Cervesato, Frank Pfenning and David Walker. Workshop on Logical Frameworks and Meta-Logics. Cork, Ireland, July 2004.
Modal Proofs as Distributed Programs (extended abstract). Limin Jia and David Walker. European Symposium on Programming Languages, April 2004.
A Concurrent Logical Framework: The Propositional Fragment. Kevin Watkins, Iliano Cervesato, Frank Pfenning and David Walker. To appear in Lecture Notes in Computer Science, special volume for the proceedings of TYPES 2003.
Aspects, Information Hiding and Modularity. Daniel S. Dantas and David Walker. Draft, November, 2003.
A Language and System for Composing Security Policies. Lujo Bauer, Jarred Ligatti and David Walker. Submitted for publication, November, 2003.
A Theory of Aspects. David Walker, Steve Zdancewic and Jay Ligatti. ACM SIGPLAN International Conference on Functional Programming, August 2003.
An Effective Theory of Type Refinements. Yitzhak Mandelbaum, David Walker and Robert Harper. ACM SIGPLAN International Conference on Functional Programming, August 2003.
Modal Proofs As Distributed Programs. Limin Jia and David Walker. Princeton University technical report TR-671-03. August 2003.
Reasoning about Hierarchical Storage. Amal Ahmed, Limin Jia and David Walker. IEEE Symposium on Logic in Computer Science. June, 2003.
Resource Usage Analysis Via Scoped Methods. Gang Tan, Xinming Ou and David Walker. Workshop on Foundations of Object-Oriented Languages. January, 2003.
The Logical Approach to Stack Typing. Amal Ahmed and David Walker. ACM SIGPLAN Workshop on Types in Language Design and Implementation. January, 2003.
A Concurrent Logical Framework I: Judgments and Properties. Kevin Watkins, Iliano Cervesato, Frank Pfenning and David Walker. Carnegie Mellon University Technical Report CMU-CS-02-101. March 2002; revised May 2003.
A Concurrent Logical Framework II: Examples and Applications. Iliano Cervesato, Frank Pfenning, David Walker and Kevin Watkins. Carnegie Mellon University Technical Report CMU-CS-02-102. March 2002; revised May 2003.
Types and Effects for Non-interfering Program Monitors. Lujo Bauer, Jarred Ligatti and David Walker. International Symposium on Software Security. Tokyo, November, 2002. Revised for printing in Software Security -- Theory and Systems, LNCS 2609, Springer, pp 154--171. December 2002.
A Calculus for Composing Run-time Security Policies. Lujo Bauer, Jarred Ligatti and David Walker. Princeton University Technical Report TR-655-02. August, 2002.
More Enforceable Security Policies. Lujo Bauer, Jarred Ligatti and David Walker. In the Workshop on Foundations of Computer Security (FCS 02). Copenhagen, July 2002.
More Enforceable Security Policies. Lujo Bauer, Jarred Ligatti and David Walker. Princeton University Technical Report TR-649-02. June 2002.
On Regions and Linear Types. David Walker and Kevin Watkins. In the International Conference on Functional Programming, Florence, Sept. 2001.
Alias Types for Recursive Data Structures. David Walker and Greg Morrisett. In the Workshop on Types in Compilation, Montreal. Selected and revised papers printed in LNCS 2071 (Harper, ed.) March 2001.
On Regions and Linear Types. David Walker and Kevin Watkins. In the Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, London, Jan. 2001.
Typed Memory Management. David Walker. PhD Thesis, Cornell University. January 2001.
Alias Types. Fred Smith, David Walker and Greg Morrisett. In the European Symposium on Programming, Berlin, March 2000. Published in Gert Smolka, editor, Lecture Notes in Computer Science, volume 1782, pages 366-381.
A Type System for Expressive Security Policies. David Walker. 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.
TALx86: A Realistic Typed Assembly Language. Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. In the ACM SIGPLAN Workshop on Compiler Support for System Software, INRIA Research Report 0228, pages 25-35, Atlanta, May 1999.
Typed Memory Management in a Calculus of Capabilities. David Walker, Karl Crary, and Greg Morrisett. Technical Report TR2000-1780, Cornell University, February 2000.
A Type System for Expressive Security Policies (Extended version). David Walker. Technical Report TR99-1740, Cornell University, April 1999.
Typed Memory Management in a Calculus of Capabilities. Karl Crary, David Walker, and Greg Morrisett. In the Twenty-Sixth ACM Symposium on Principles of Programming Languages , pages 262-275, San Antonio, Jan. 1999.
Stack-Based Typed Assembly Language. Greg Morrisett, Karl Crary, Neal Glew, and David Walker. 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.
From System F to Typed Assembly Language. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. In the Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85-97, San Diego, Jan. 1998.
From System F to Typed Assembly Language (Extended version). Greg Morrisett, David Walker, Karl Crary, and Neal Glew. Technical Report TR97-1651, Cornell University, November 1997.
Teaching, Princeton University
COS 226: Algorithms & Data Structures. Spring 2007
COS 320: Compiling Techniques. Spring 2003, Spring 2004, Spring 2005, Spring 2006.
COS 441: Programming Languages. Fall 2005.
COS 510: Programming Languages. Fall 2002, Fall 2003.
COS 597B: Computer Security Foundations. Fall 2004.
COS 598E: Foundations of Language-Based Security. Spring 2002.
TACL Seminar. An advanced research seminar on programming languages, compilers and tools. Fall 2002 --.
Students
Ph.D Students (Graduated)
Jay Ligatti. Graduated May 2006. First position: Assistant Professor, University of South Florida.
Yitzhak Mandelbaum. Graduated August 2006. First position: Researcher, AT&T Labs Research.
Ph.D. Students (Current)
Dan Dantas. General exam, Jan 2005.
Limin Jia. Pre-FPO, Oct 2006.
Frances Spalding. General exam, Jan 2005.
Ph. D. Committees
Zhaozhong Ni, Ph.D. Yale University (2006) Modular Machine Code Verification.
Spyridon Triantafyllis, Ph.D. (2006) Eliminating Scope and Selection Restrictions in Compiler Optimizations.
Dinghao Wu. Ph.D. (2005) Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code
Gang Tan. Ph.D. (2005) A Compositional Logic for Control-flow and its Application in Foundational Proof-Carrying Code.
Xinming Ou. Ph.D. (2005) A Logic-Programming Approach to Network Security.
Eun-Young Lee, Ph.D. (2004) Secure Linking: A Logical Framework for Policy-Enforced Component Composition.
Juan Chen, Ph.D. (2004) A Low-Level Typed Assembly Language with a Machine-checkable Soundness Proof.
Amal Ahmed. Ph.D. (2004) Semantics of Types for Mutable State.
Yitzchak (Zuki) Gottlieb. Ph.D. (2004) Operating System Support for Generalized Packet Forwarding.
Kedar N. Swadi, Ph.D. (2003) Typed Machine Language.
Lujo Bauer, Ph.D. (2003) Access Control for the Web via Proof-Carrying Authorization.
Undergraduate Research
Zach Devito, Junior Independent Work (Fall 06)
Ben DeLoache, Junior Independent Work (Fall 06)
Lester Mackey, Junior Independent Work (Spring 06)
Winner of CRA Outstanding Undergraduate Award, in part due to
this undergraduate research.
Jin Oh, Senior Independent Work (Spring 06)
Mark Daly. Senior Thesis. Fall 2005-Spring 2006.
Michael Ten-Pow. Junior Independent Work. Fall 2005.
Rob Simmons. Senior Thesis, Fall 2004-Spring 2005.
Co-winner of the Princeton Computer Science Department Senior Thesis Award.
Jonathon Heinberg. Junior Independent Work, Spring 2003.
Jonathon Heinberg. Junior Independent Work, Fall 2002.
Bismark Paliz. Senior Independent Work, Fall 2002.
Teaching, Cornell University
Instructor: Introductory C Programming (100 level). Fall 1997.
Cornell Computer Science Outstanding TA Award. May 1996.
Teaching Assistant: Software Engineering (500 level). Fall 1996.
Teaching Assistant: Computers and Programming (200 level). Spring 1996 Fall 1995.
Academic Service
ACM SIGPLAN Workshop on Programming Languages and Analysis for Security. Program Committee, 2007.
Trends in Functional Programming. Program Committee, 2007.
ACM SIGPLAN Symposium on Principles of Programming Languages. Program Committee, 2007.
ACM SIGPLAN International Symposium on Code Generation & Optimization. Program Committee, 2007.
Workshop on Foundations of Object-Oriented Languages, Program Committee, 2007.
The
Computer Science Futures Project, a DARPA-sponsored panel on the
future of computer science research. Panelist, 2006.
ACM/NSF Summer School on Language-Based Techniques for Concurrent and Distributed Software. Steering Committee. July 2006.
33rd International Colloquium on Automata, Languages and Programming. Program Committee, 2006.
Workshop on Foundations of Aspect-Oriented Languages, Program Committee, 2006
Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. Program Co-chair, 2006.
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Publicity Chair, 2003-2006.
ACM/NSF Summer School on Reliable Computing. Organizing committee (co-chair). Eugene, OR, July 2005.
Workshop on Foundations of Aspect-Oriented Languages, Program Chair, 2005.
Workshop on Logics for Resources, Processes and Programs, Program Committee, 2004.
ACM/NSF Summer School on Security: Theory to Practice. Organizing committee (co-chair). Eugene, OR, June 2004.
ACM SIGPLAN International Conference on Functional Programming (ICFP), Program Committee, 2004.
ACM SIGPLAN International Workshop on Types in Language Design and implementation, Program Committee, 2004.
Workshop on Foundations of Aspect-Oriented Languages, Program Committee, 2004.
New Jersey Programming Languages Seminar (NJPLS), Host, September 2003.
ACM-NSF Summer School on Foundations of Security. Invited Lecturer. Eugene, OR, June 2003.
New Jersey Programming Languages Seminar (NJPLS), Program Chair, December, 2002.
ACM State-of-the-art Summer School on Foundations of Internet Security. Invited Lecturer. Poland, June 2002.
Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM), Program committee, January 2002.
Panelist for a number of NSF funding programs.
Referee for workshops, conferences and journals on programming languages
Including (among many others) Transactions on Programming Languages and Systems (TOPLAS), Journal of Functional Programming (JFP), Journal of Automated Reasoning (JAR), Journal of Higher-order and Symbolic Computation (HOSC); ACM SIGPLAN Conferences on Functional Programming (ICFP), Principles of Programming Languages (POPL), and Programming Language Design and Implementation (PLDI); Other conferences including the European Symposium on Programming (ESOP), the European Conference on Object-oriented Programming (ECOOP).
Selected Invited Talks
Cosmic Rays, Bat Droppings and What We Can Do About Them. Yale
University Computer Science Department Colloquium. Nov 2006.
Cosmic Rays, Bat Droppings and What We Can Do About Them. IFIP Working Group 2.8. July 2006.
PADS/ML: A Functional Data Description Language. Carnegie Mellon POP Seminar. Invited talk. May 2006.
Logics for Checking Properties of Pointer Programs. IMLA, Chicago, US. June 2005.
Stacks, Heaps and Regions: One Logic to Bind Them. SPACE 2004, Venice, Italy. January 2004.
Software Security Monitors: Theory and Practice. Stevens Institute, Hoboken NJ. December 2003.
Software Security Monitors: Theory and Practice. UC Berkeley, Berkeley CA. July 2003.
Software Security Monitors: Theory and Practice. Intel Research, Santa Clara CA. July 2003.
Poly Stop a Hacker. New Jersey Programming Languages Seminar. September, 2002.
A Concurrent Logical Framework. Symposium on Cyber Security and Trustworthy Software. Stevens Institute, New York, March 15, 2002.
Secure Certifying Compilation. IBM T. J. Watson, New York, April 12, 2000.
Education
Cornell University: Ph.D. in Computer Science, Aug 95 - Jan 2001.Employment Experience
Assistant Professor, Princeton University (February 2002-present)
Postdoctoral Fellow, Carnegie Mellon University (September 2000 - October 2001)Teaching Assistant, Cornell University (Fall 95 - Fall 97)
Kandalore Camp (Summer 91-93, 95, 96)Funding
Real-Time Network Forensic Analysis. DARPA subcontract under prime contract number FA8750-07-C-0014 (PI). $79,329. Jan 2007 - June 2007.
Well-typed,
Trustworthy Computing in the Presence of Transient Faults. NSF award
CNS-0627650 (PI). $1.1 million. August 2006 - August 2010.
Language Support for Data-centric Systems Monitoring. NSF award CNS 0615062
(PI). $798,975. July 2006 - July 2009.
Automatic Tool Generation for Ad Hoc Scientific Data. NSF award IIS 0612147
(PI). $493,124. July 2006 - July 2009.
Collaborative Research: CSR-PDOS: Managing OS Extensibilty via Aspect-oriented
Programming Technology. NSF award CSR 0615213
(Co-PI). $315,319. July 2006 - July 2009.
Emerson Junior Faculty Award for Excellence in Research and Teaching. May 2005.
Alfred P. Sloan Fellow. Sept 2004-Sept 2006.
Assurance-Carrying Components. ARDA grant for BAA 03-03-FH, Co-PI. Oct 2003-March 2005.
CAREER: Programming Languages for Secure and Reliable Component Software Systems. NSF Career Grant, CCR-0238328, PI. July 2003-June 2008.
Collaborative Research: High-Assurance Common Language Runtime. NSF CCR-0208601, Co-PI. July 2002-June 2007.
A Gift from Microsoft Research. PI. February 2002.
Scaling Proof-Carrying Code to Production Compilers and Security Policies. DARPA contract F30602-99-1-0519, Co-PI. December 2002-December 2003.
Efficient Logics For Network Security. ONR. Senior personnel (Carnegie Mellon University). February 2001-January 2002.