Research Topics

The overall goal of my research is to identify important, practical problems in software construction, to study the formal properties of the problematic software, often through the lens of type theory, and to propose novel, effective, and provably correct solutions.  Working in this model over the past few years, I have focused on answering the following specific research questions.

How do we program productively and reliably with ad hoc data?

How do we guarantee software is reliable when hardware may exhibit transient faults?

How do we develop correct, modular security monitoring infrastructure?

How do we guarantee that programs doing their own memory management do so safely?

How do we provide a provably safe, yet flexible low-level platform for mobile code?

Below I have organized a selection of my papers around the central topics list above (as well as a final category of others).  I placed a symbol beside those papers I'm really fond of and think are representative of my very best research.  I limited myself to at most 2 such papers in each category -- in a couple of cases, it was very difficult to choose.  I didn't select these papers based on the level of prestige of the venue in which they were first presented.  They are my personal assessment of which papers I believe are my most creative, original and important.  I also included references to the Ph.D. theses of students I have advised.  For a more complete and usually more up-to-date list of papers, please view my chronological list.  You may also wish to see my CV.

Copyright note 

Ad Hoc Data

LearnPADS:  Fully Automatic Tool Generation From Ad Hoc Data. Kathleen Fisher, David Walker and Kenny Q. Zhu.  ACM SIGMOD Demo Session.  To appear June 2008.(pdf)

From Dirt to Shovels:  Fully Automatic Tool Generation From Ad Hoc Data. Kathleen Fisher, David Walker, Kenny Q. Zhu and Peter White.  To appear at the ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages.  January 2008.(pdf)

From Dirt to Shovels:  Fully Automatic Tool Generation From Ad Hoc Data.  David Walker.  Invited talk.  AT&T UC Symposium 2007. (ppt)

Towards 1-click Tool Generation with PADS. David Burke, Kathleen Fisher and David Walker, Peter White and Kenny Q. Zhu.  In the ICML-2007 Workshop on Challenges and Applications of Grammar Induction.  June 2007. (pdf)

Towards 1-click Tool Generation with PADS.  David Walker.  ICML-2007 Workshop on Challenges and Applications of Grammar Induction.  June 07.  (ppt)

A Dual Semantics for the Data Description Calculus (Extended Abstract).  Yitzhak Mandelbaum, Kathleen Fisher and David Walker.  In the Eighth Symposium on Trends in Functional Programming, April 2007.  (pdf)

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

The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum, David Walker. Draft generated December 2006.  (pdf)

The Theory and Practice of Data Description.  Yitzhak Mandelbaum, Ph.D. thesis, Princeton University.  Archived as Princeton University technical report TR-764-06, August 2006. (abstract, pdf)

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

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 paper.  June 2006. (pdf)

PADS/ML: A Functional Data Description Language.  Carnegie Mellon POP Seminar.  May 06.  (ppt)

The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum and David Walker.  ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages.  January 2006.  (pdf)

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

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

PADS: Simplified Data Processing for Scientists.  Princeton Junior Faculty Seminar.  March 05. (ppt)

Reliability in the Presence of Transient Faults

Fault-tolerant Typed Assembly Language. Frances Perry, Lester Mackey, George A. Reis, Jay Ligatti, David I. August, and David Walker.  ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2007.  Winner of the PLDI 07 Best Paper Award. (pdf) 

Fault-tolerant Typed Assembly Language (Extended Version). Frances Perry, Lester Mackey, George A. Reis, Jay Ligatti, David I. August, and David Walker.   Princeton technical report number TR-776-07.  April 2007. (pdf) 

On Cosmic Rays and What To Do About Them. Yale University Computer Science Department Colloquium.  November 06. (ppt)

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

On Cosmic Rays, Bat Droppings and What We Can Do About Them. WG 2.8.  Invited talk.  July 06. (ppt)

Security Monitoring

Composing Expressive Run-time Security Policies.  Lujo Bauer, Jay Ligatti, and David Walker.  Draft generated February 2007.  Accepted for publication in ACM Transactions on Software Engineering and Methodology, November 2007. (pdf)

Run-time Enforcement of Nonsafety Policies. Jay Ligatti, Lujo Bauer, and David Walker. Draft generated, January 2007. (pdf)

AspectML: A Polymorphic Aspect-oriented Functional Programming Language.  Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich.  Generated March 2006.  Accepted for publication in ACM Transactions on Programming Languages and Systems, April 2007. (pdf)

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. (preprint version:  ps)

Policy Enforcement via Program Monitoring. Jarred Adam Ligatti. PhD thesis, Princeton University.  Archived as Princeton University technical report TR-752-06, May 2006.  (abstract, pdf)

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

Harmless Advice.  Daniel S. Dantas and David Walker.  ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages.  January 2006. (pdf)

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

Enforcing Non-safety Security Policies with Program Monitors. Jay Ligatti, Lujo Bauer and David Walker. Tenth European Symposium on Research in Computer Security.  September 2005 (pdf). 

Patch(1) Considered Harmful.  Marc E. Fiuczynski, Robert Grimm, Yvonne Coady and David Walker.  Workshop on Hot Topics in Operating Systems.  June, 2005.  (pdf)

Composing Security Policies in Polymer.  Lujo Bauer, Jay Ligatti and David Walker.  ACM SIGPLAN Conference on Programming Language Design and Implementation. June 2005. (ps)

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

Harmless Advice.  Daniel S. Dantas and David Walker.  In Foundations of Object-Oriented Languages, January 2005.  (pdf)

Aspects, Information Hiding and Modularity.  Daniel S. Dantas and David Walker.  November, 2003.  Princeton University Technical Report TR-696-04. (pdf)

A Theory of Aspects.  David Walker, Steve Zdancewic and Jay Ligatti.  In the ACM SIGPLAN International Conference on Functional Programming, August 2003. (pdf)

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

More Enforceable Security Policies.  Lujo Bauer, Jarred Ligatti and David Walker.  Workshop on Computer Security Foundations.  Copenhagen, July 2002.  (pdf)

A Type System for Expressive Security Policies.  David Walker.  Twenty-Seventh ACM SIGPLAN Symposium on Principles of Programming Languages . pages 254-267, Boston, January 2000.  (pdf)  A previous version of this paper appeared in the FLOC '99 Workshop on Run-time Result Verification. Trento, Italy, July 1999.

Safe Memory Management

Linear Logic, Heap-shape Patterns and Imperative Programming.  Limin Jia and David Walker.  Princeton University Technical Report TR-762-06. July, 2006. (pdf)

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

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

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

A Refined Proof Theory for Reasoning About Separation.  Limin Jia and David Walker.  IEEE Symposium on Logic in Computer Science, short paper.  June 2005.  (pdf)

Substructural Type Systems.  Chapter 1 of Advanced Topics in Types in Programming Languages, Benjamin Pierce, ed.,  January 2005.

Stacks, Heaps and Regions: One Logic to Bind Them.  SPACE 04.  Invited talk. January, 04. (ppt)

Reasoning about Hierarchical Storage.  Amal Ahmed, Limin Jia and David Walker.  IEEE Symposium on Logic in Computer Science, pp. 33-44. Ottawa, Canada, June 2003. (pdf)

On Linear Types and Regions.  David Walker and Kevin Watkins. In ACM SIGPLAN International Conference on Functional Programming, September 2001. (pdf)  A previous version of this work appeared in the Workshop on Semantics, Program Analysis and Computing Environments for Memory Management. London, UK, January 2001.  (pdf)

Alias Types for Recursive Data Structures.  David Walker and Greg Morrisett.  Workshop on Types in Compilation. Montreal, Canada.  Selected and revised papers printed in LNCS 2071 (Harper, ed.) March 2001.  (pdf)

Typed Memory Management.  David Patrick Walker.  Cornell University. January, 2001.  (pdf)

Typed Memory Management via Static Capabilities.  David Walker, Karl Crary, and Greg Morrisett.  ACM Transactions on Programming Languages and Systems, 22(4):701-771, July 2000.  (pdf)

Alias Types.  Frederick Smith, David Walker, and Greg Morrisett.  European Symposium on Programming. Published in Lecture Notes in Computer Science, Gert Smolka, editor, volume 1782, 366-381, Berlin, Germany, March 2000.  (pdf)

Typed Memory Management in a Calculus of Capabilities.  Karl Crary, David Walker, and Greg Morrisett.  Twenty-Sixth ACM SIGPLAN Symposium on Principles of Programming Languages. pages 262-275, San Antonio, January 1999.

Typed Assembly Language

The Logical Approach to Stack Typing.  Amal Ahmed and David Walker.  ACM workshop on Types in Language Design and Implementation. January, 2003.  (pdf)

An Introduction to Typed Assembly Language.  2.5 weeks of comprehensive lecture notes from COS 598E: Foundations of language-based security.  David Walker adapted from Greg Morrisett.  March 2002. (pdf)

Stack-based Typed Assembly Language.  Greg Morrisett, Karl Crary, Neal Glew, and David Walker.  Journal on Functional Programming, 12(1):43-88, January 2002.  (pdf)

From System F to Typed Assembly Language.  Greg Morrisett, David Walker, Karl Crary, and Neal Glew.  ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999.  (pdf)

TALx86: A Realistic Typed Assembly Language.  Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, Dave Walker, Stephanie Weirich, and Steve Zdancewic.  In the ACM SIGPLAN Workshop on Compiler Support for System Software. pages 25-35, Atlanta, May 1999.  (pdf)

Stack-Based Typed Assembly Language.  Greg Morrisett, Karl Crary, Neal Glew, and David Walker.  1998 Workshop on Types in Compilation (TIC '98). Kyoto, Japan. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28-52. Springer, 1998.  (pdf)

From System F to Typed Assembly Language.  Greg Morrisett, David Walker, Karl Crary, and Neal Glew. Twenty-Fifth ACM SIGPLAN Symposium on Principles of Programming Languages. pages 85-97, San Diego, January 1998.  (pdf)

Others

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.  To appear, September 2006. (pdf)

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

Modal Proofs As Distributed Programs (extended abstract).  Limin Jia and David Walker.  In the European Symposium on Programming, LNCS 2986, David Schmidt (Ed.), pp. 219--233, Springer, April, 2004. (pdf)  See below for an extended technical report on this topic.

An Effective Theory of Type Refinements.  Yitzhak Mandelbaum, David Walker and Robert Harper.  In the ACM SIGPLAN International Conference on Functional Programming, August 2003. (pdf)

A Concurrent Logical Framework:  The Propositional Fragment.  Kevin Watkins, Iliano Cervesato, Frank Pfenning and David Walker.  In S. Berari, M. Coppo, and F. Damiani, Ed,  Types for Proofs and Programs, Lecture Notes in Computer Science 3085, Springer-Verlag, pages 355-377, 2004.  Revised selected papers and from the Third International Workshop along the Types for Proofs and Program, Torino, Italy, April 2003.(pdf)  See below for two technical reports on this topic.

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

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

Resource Usage Analysis Via Scoped Methods. Gang Tan, Xinming Ou and David Walker.  Foundations of Object-Oriented Languages. January, 2003.  (pdf)