David Walker

Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
David Walker

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: 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 distributed computing; language-based security and run-time security monitoring.

Books and Journal Articles

	A Type-Theoretic Interpretation of Pointcuts and Advice. Jay Ligatti, David Walker and Steve Zdancewic. Science of Computer Programming. Submitted March 2005, accepted (pending minor revisions) July 2005.
	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

	The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum and David Walker. ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages. To appear, January 2006.
	Harmless Advice. Daniel S. Dantas and David Walker. ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages. To appear, 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. To appear, 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.
	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. (pdf) See below for an extended technical report on this topic.
	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 320: Compiling Techniques. Spring 2003.
	COS 510: Programming Languages. Fall 2002, Fall 2003.
	TACL Seminar. An advanced research seminar on programming languages, compilers and tools. Fall 2002. Spring 2003.
	COS 598E: Foundations of Language-Based Security. Spring 2002.

Students

Ph. D. Students (Princeton University)

Dan Dantas. Aspect-oriented programming and security.

General exam (Jan 2005): Harmless advice.

Advised since March 2003.

Limin Jia. Substructural logics for automated reasoning about memory management.

General exam (May 2003): Modal proofs as distributed programs.

Advised since Feb 2002.

Jarred Ligatti. Run-time security monitoring: theory and practice.

Thesis (graduation expected Spring 2006): Policy Enforcement via Program Monitoring.

Pre-FPO (Sep 2005): Policy Enforcement via Program Monitoring

General exam (May 2003): Run-time policy enforcement with edit automata.

Advised since Feb 2002.

Yitzhak Mandelbaum. Processing Ad Hoc Data Sources.

General exam (May 2003): An effective theory of type refinements.

Advised since Feb 2002.

Frances Spalding

General exam (Jan 2005): Certifying compilation for a language with stack allocation.

Ph. D. Committees

Kedar N. Swadi, Ph.D. (2003) Typed Machine Language.

Lujo Bauer, Ph.D. (2003) Access Control for the Web via Proof-Carrying Authorization.

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. (2004) Semantics of Types for Mutable State.

Yitzchak (Zuki) Gottlieb (2004) Operating System Support for Generalized Packet Forwarding.

Dinghao Wu. (2005) Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code

Gang Tan. (2005) A Compositional Logic for Control-flow and its Application in Foundational Proof-Carrying Code.

Xinming Ou. (2005) A Logic-Programming Approach to Network Security.

Undergraduates (Princeton University)

Mark Daly, A User Interface and Format Inference for Processing Ad Hoc Data. Senior Thesis. Fall 2005-Spring 2006.

Michael Ten-Pow. Junior Independent Work. Fall 2005.

Rob Simmons, Twelf as a Unified Framework for Language Formalization and Implementation. Senior Thesis, Fall 2004-Spring 2005. Co-winner of the Princeton Computer Science Department Senior Thesis Award.

Jonathon Heinberg, MinAML: A Minimalized Aspect-oriented Programming Language. Junior Independent Work, Spring 2003.

Jonathon Heinberg, JTensor: A Linear Logic Theorem Prover in Java. Junior Independent Work, Fall 2002.

Bismark Paliz, Engineering Webservers for Resistance to Denial of Service Attacks. 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.

Other Academic Activities

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Program Committee, 2007.

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.

NSF ITR review panel, 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.

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).

Some Recent Invited Talks

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.

	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)

Employment Experience

Assistant Professor, Princeton University (February 2002-present)

Postdoctoral Fellow, Carnegie Mellon University (September 2000 - October 2001)

	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 children aged 11-15.

Funding

	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.