Research Documents

See below for most of my publications (and some work-in-progress), my thesis, most of my technical reports and some selected talks organized chronologically.  See this page for a selection of papers organized by topic.  I have also listed my funding sources.  You may also wish to see my CV.

Copyright Note

Publications (and some work-in-progress), Chronological Order 

[2008]

Reasoning about Control Flow in the Presence of Transient Faults. Frances Perry and David Walker.   To appear in the 15th International Static Analysis Symposium July 2008. (pdf)

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.  ACM SIGPLAN-SIGACT Symposium on Principles of Programming languages.  January 2008.(pdf)

[2007]

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)

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

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)

Run-time Enforcement of Nonsafety Policies. Jay Ligatti, Lujo Bauer, and David Walker. Journal draft generated January 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)

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

[2006]

The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum, David Walker. Draft generated December 2006.  (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)

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)

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)

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

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)

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)

Harmless Advice.  Daniel S. Dantas 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)

[2005]

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)

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)

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)

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

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

[2004]

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.

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.

[2003]

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

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) See below for an extended technical report on this topic.

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)

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

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

[2002]

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)

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)

[The younger years -- prior to 2002]

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

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.

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)

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.

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.  Winner of the Most Influential 1998 POPL Paper Award (awarded 10 years later at POPL 2008). (pdf)

Thesis

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

Technical Reports, Notes and Other Writing

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)

Linear Logic, Heap-shape Patterns and Imperative Programming.  Limin Jia and David Walker.  Princeton University Technical Report TR-762-06. July, 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)

PolyAML: A Polymorphic Aspect-oriented Functional Programming Language (Extended Version). Daniel S. Dantas, David Walker, Geoffrey Washburn and Stephanie Weirich.  University of Pennsylvania Computer and Information Science Technical Report MS-CIS-05-07. Generated May 2005.  Revised Sept 2005. (pdf)

Enforcing non-safety security policies with program monitors. Jay Ligatti, Lujo Bauer, and David Walker. Technical Report TR-720-05, Princeton University, January 2005. (pdf)

Analyzing Polymorphic Advice.  Daniel S. Dantas, David Walker, Geoffrey Washburn and Stephanie Weirich.  Short paper, October 2004 (pdf).  Longer version, Princeton University Technical Report TR-717-04, December 2004 (pdf).

Dynamic Typing with Dependent Types.  Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker.  Princeton University Technical Report TR-695-04, April 2004.  (pdf)

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

Modal Proofs As Distributed Programs.  Limin Jia and David Walker.  Princeton University technical report TR-671-03.  August 2003. (pdf)

Modal Proofs As Distributed Programs.  Limin Jia and David Walker.  July 2003.  (pdf)  A short version of the technical report above.

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)

An Effective Theory of Type Refinements.  Yitzhak Mandelbaum, David Walker and Robert Harper.  Princeton Technical Report TR-656-02, December 2002.  (pdf)

Modular Run-time Program Monitors.  David Walker.  A talk at the International Symposium on Software Security.  Tokyo, November 2002. (slides)

A Concurrent Logical Framework:  The Propositional Fragment.  Kevin Watkins, Iliano Cervesato, Frank Pfenning and David Walker.  October, 2002.  (pdf)

A Calculus for Composing Security Policies.  Lujo Bauer, Jarred Ligatti and David Walker.  Princeton University Technical Report TR-655-02. August, 2002.  (pdf)

More Enforceable Security Policies.  Lujo Bauer, Jarred Ligatti and David Walker.  Princeton University Technical Report TR-649-02.  June 2002.  (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)

A Concurrent Logical Framework.  Symposium on Cyber-Security.  Stevens Institute, Hoboken NJ.  March 2002.  (slides)

CLF: A Concurrent Logical Framework.  Iliano Cervesato, Frank Pfenning, David Walker and Kevin Watkins.  January 2002.  (pdf)

Mechanical Reasoning About Low-level Programs.  David Walker.  Unpublished notes from lectures given in John Reynolds course on reasoning about low-level programs. March 2001. (pdf)

Alias Types for Recursive Data Structures (Extended Version).  David Walker and Greg Morrisett.  Technical Report TR2000-1787, Cornell University, March 2000. (pdf)

Typed Memory Management in a Calculus of Capabilities.  David Walker, Karl Crary, and Greg Morrisett.  Technical Report TR2000-1780, Cornell University, February 2000.

Alias Types.  Frederick Smith, David Walker, and Greg Morrisett.  Technical Report TR99-1773, Cornell University, October 1999.  (pdf)

A Type System for Expressive Security Policies (Extended version). David Walker.  Technical Report TR99-1740, Cornell University, April 1999.

Stack-Based Typed Assembly Language (Extended version).  Greg Morrisett, Karl Crary, Neal Glew, and David Walker.  Technical Report CMU-CS-98-178, Carnegie-Mellon University, December 1998.  (pdf)

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

Selected Talks

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

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

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

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

Logics for Checking Properties of Pointer Programs.  IMLA 05.  Invited talk.  June 05.

PADS:  A System for Processing Ad Hoc Data Sources.  David Walker.  Industrial Affliates, May 05. (ppt)

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