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

Chronological Order 

[2017]

A General Approach to Network Configuration Verification. Ryan Beckett, Aarti Gupta, Ratul Mahajan and David Walker. ACM SIGCOMM, August 2017. (pdf, minesweeper home, github)

Network Configuration Synthesis with Abstract Topologies. Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye and David Walker. ACM PLDI, June 2017. (pdf, propane home, github)

[2016]

Hardware-software co-design for network performance measurement. Srinivas Narayana, Anirudh Sivaraman, Vikram Nathan, Mohammad Alizadeh, David Walker, Jennifer Rexford, Vimalkumar Jeyakumar, and Changhoon Kim. Hot topics in Networks (HotNets), November 2016.

Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations. Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye and David Walker. ACM SIGCOMM, August 2016. Winner of SIGCOMM best paper award. (pdf, propane home, tutorial, github)

SNAP: Stateful Network-Wide Abstractions for Packet Processing. Mina Arashloo, Yaron Koral, Michael Greenberg, Jennifer Rexford and David Walker. ACM SIGCOMM, August 2016. (Princeton tech report TR-987-16)

Temporal NetKAT. Ryan Beckett, Michael Greenberg and David Walker. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 16), June 2016. (pdf; including extended technical appendix; PLDI 2016 Presentation)

Compiling Path Queries. Srinivas Narayana, Mina Arashloo, Jennifer Rexford, and David Walker. USENIX Symposium on Networked Systems Design and Implementation (NSDI 16), March 2016. (pdf)

CacheFlow: Dependency-Aware Rule-Caching for Software-Defined Networks. Naga Katta, Omid Alipourfard, Jennifer Rexford, David Walker. ACM SIGCOMM Symposium on SDN Research (SOSR 16), March 2016. Winner of the SOSR'16 best paper award! (pdf)

Example-Directed Synthesis: A Type-theoretic Interpretation. Jonathan Frankle, Peter-Michael, David Walker, and Steve Zdancewic In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 16), January 2016. (pdf)

Confluences in Programming Languages Research. David Walker. ACM SIGPLAN Robin Milner Award Lecture. At the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 16), January 2016. (abstract) (video) (keynote slides) (pdf slides)

[2015]

CoVisor: A Compositional Hypervisor for Software-Defined Networks. Xin Jin, Jennifer Gossels, Jennifer Rexford, and David Walker. USENIX Symposium on Networked Systems Design and Implementation (NSDI 16), May 2015. (website) (pdf)

Tracking the Flow of Ideas through the Programming Languages Literature. Michael Greenberg, Kathleen Fisher, and David Walker. SNAPL: The Inaugural Summit on Advances in Programming Languages, May 2015. (website) (pdf)

Temporal NetKAT Ryan Beckett, Michael Greenberg, and David Walker. PLVNET: 1st Workshop on Programming Languages and Verification Technology for Networking. January 2015. (pdf)

Type systems for SDN Controllers. Marco Gaboardi, Michael Greenberg and David Walker. PLVNET: 1st Workshop on Programming Languages and Verification Technology for Networking. January 2015. (pdf)

[2014]

Transparent, Live Migration of a Software-defined Network. Soudeh Ghorbani, Cole Schlesinger, Matthew Monaco, Eric Keller, Matthew Caesar, Jennifer Rexford, and David Walker. ACM Symposium on Cloud Computing. November, 2014. (pdf)

Concurrent NetCore:  From Policies to Pipelines.  Cole Schlesinger, Michael Greenberg and David Walker.  ACM SIGPLAN International Conference on Functional Programming (ICFP).  September 2014. (pdf)

Compiling Path Queries in Software-defined Networks. Srinivas Narayana, Jennifer Rexford, and David Walker.  ACM SIGCOMM HotSDN Workshop, August 2014.  (pdf)

An Assertion Language for Debugging SDN Applications.  Ryan Beckett, X. Kelvin Zou, Shuyuan Zhang, Sharad Malik, Jennifer Rexford, and David Walker. ACM SIGCOMM HotSDN Workshop, August 2014.  (pdf)

Incremental Update for a Compositional SDN Hypervisor.  Xin Jin, Jennifer Rexford, and David Walker.  ACM SIGCOMM HotSDN Workshop, August 2014. (pdf)

Infinite CacheFlow in Software-defined Networks.  Naga Katta, Omid Alipourfard, Jennifer Rexford, and David Walker.  ACM SIGCOMM HotSDN Workshop, August 2014. (pdf)  An earlier version appeared as Princeton Computer Science Technical Report TR-966-13, October 2013.

Hone:  Joint Host-Network Traffic Management in Software-Defined Neteworks.  Peng Sun, Minlan Yu, Michael Freedman, Jennifer Rexford and David Walker.  To appear in the Journal of Network and Systems Management.  2014. (pdf)

Programming Protocol-independent Packet Processors, Pat Bosshart, Dan Daly, Martin Izzard, Nick McKeown, Jennifer Rexford, Dan Talayco, Amin Vahdat, George Varghese and David Walker.  Computer and Communications Review (CCR).  Volume 44, Issue 3.  July 2014.  (pdf An earlier version in arXiv, December 2013.

Modular Protections against Non-control Data Attacks. Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker, and Benjamin Zorn.  To appear in the Journal of Computer Security.  2014. (pdf)

NetKAT: Semantic Foundations for Networks.  Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker.  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. January 2014. (ACM Digital Library) (pdf).

Extended technical report issued by Cornell University October 2013 at http://hdl.handle.net/1813/34445.

The Frenetic Project:  Declarative Languages for Programming Networks.  Invited talk at the ACM Symposium on Practical Applications of Declarative Languages (PADL) 2014. (abstract)

[2013]

Programming protocol-independent packet processors, Pat Bosshart, Dan Daly, Martin Izzard, Nick McKeown, Jennifer Rexford, Dan Talayco, Amin Vahdat, George Varghese and David Walker.  In arXiv, December 2013.  (link)

Optimizing the "One Big Switch" Abstraction in Software-Defined Networks.  Nanxi Kang, Zhenming Liu, Jennifer Rexford and David Walker.  ACM CoNext, December 2013.  (pdf)

Infinite CacheFlow in Software-Defined Networks.  Naga Katta, Jennifer Rexford and David Walker.  Princeton Technical Report TR-966-13, October 2013.  (Technical Report).

Modular SDN Programming with Pyretic.  Josh Reich, Chris Monsanto, Nate Foster, Jen Rexford, and David Walker.  USENIX ;login Magazine.  38(5):128-134, October 2013.  (pdf preprint) (official version)

Incremental Consistent Updates.  Naga Katta, Jennifer Rexford and David Walker.  ACM SIGCOMM Workshop on Hot Topics in Software-Defined Networking.  August 2013.  (pdf)

An Efficient Distributed Implementation of One Big Switch.  Nanxi Kang, Zhenming Liu, Jennifer Rexford and David Walker.  Open Networking Summit, April 2013. (pdf)

Composing Software-Defined Networks.  Chris Monsanto, Josh Reich, Nate Foster, Jen Rexford, and David Walker.  USENIX NSDI, April 2013.  Winner of the NSDI Community Award. (pdf)  Pyretic project page.

Languages for Software-Defined Networks. Nate Foster, Michael J. Freedman, Arjun Guha, Rob Harrison, Naga Praveen Katta, Christopher Monsanto, Joshua Reich, Mark Reitblatt, Jennifer Rexford, Cole Schlesinger, Alec Story, and David Walker.  IEEE Communications Magazine, 51(2):128-134, February 2013. (IEEE version)

[2012]

Logic Programming for Software-Defined Networks.  Naga Praveen Katta, Jennifer Rexford and David Walker.  ACM SIGPLAN Workshop on Cross-model Language Design and Implementation, September 2012. (pdf)

Abstractions for Network Update.  Mark Reittblatt, Nate Foster, Jen Rexford, Cole Schlesinger and David Walker.  ACM SIGCOMM, August 2012.  (pdf).

A Compiler and Run-time System for Network Programs. Christopher Monsanto, Nate Foster, Rob Harrison, David Walker. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2012. (pdf).

LearnPADS++:  Incremental inference of Ad Hoc Data Formats.  Kenny Q. Zhu, Kathleen Fisher and David Walker.  ACM SIGPLAN International Symposium on Practical Aspects of Declarative Languages.  January 2012.  (pdf)

Language Abstractions for Software-Defined Networks. Nate Foster, Michael Freedman, Rob Harrison, Christopher Monsanto, Mark Reitblatt, Jennifer Rexford, Alec Story and David Walker.  Workshop on Languages for Distributed Algorithms.  January 2012. (pdf)

[2011]

A Survey of the Practice of Computational SciencePrakash Prabhu, Thomas B. Jablin, Arun Raman, Yun Zhang, Jialu Huang, Hanjun Kim, Nick P. Johnson, Feng Liu, Soumyadeep Ghosh, Stephen Beard, Taewook Oh, Matthew Zoufaly, David Walker, David I. August.  SC 11: The  International Conference for High Performance Computing, Networking, Storage and Analysis. November 2011.  (pdf)

Consistent Updates for Software-defined Networks:  Change You Can Believe In.  Mark Reittblatt, Nate Foster, Jen Rexford and David Walker.  HotNets X, November 2011. (pdf)

Frenetic: A Network Programming Language.  Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story and David Walker.  ACM SIGPLAN International Conference on Functional Programming, September 2011. (pdf)

Modular Protections against Non-control Data Attacks. Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker and Ben Zorn. Computer Security Foundations Symposium. June 2011. (pdf)

Frenetic: A Network Programming Language.  Invited talk.  Microsoft Research, Redmond.  June, 2011. (ppt)

Forest: A Language and Toolkit for Programming with Filestores.  Kathleen Fisher, Nate Foster, David Walker and Kenny Q. Zhu.  ACM SIGPLAN International Conference on Functional Programming, September 2011. (pdf)

The PADS project: An Overview.  Kathleen Fisher and David Walker.  Invited paper.  IEEE International Conference on Database Theory. March 2011.  (pdf)

Linear Maps.  Shuvendu Lahiri, Shaz Qadeer and David Walker.  ACM SIGPLAN Workshop on Programming Languages meets Program Verification.  January 2011.  (pdf)  (Extended Princeton Technical Report TR-884-10, September 2010) (pdf)

[2010]

Frenetic: A High-Level Language for OpenFlow Networks.  Nate Foster, Rob Harrison, Michael J. Freedman, Jennifer Rexford and David Walker.  Cornell Technical Report.  Handle:  http://hdl.handle.net/1813/19310 December 2010. (tr)

Forest:  A Language and Toolkit For Programming with Filestores.  Kathleen Fisher, Nate Foster, David Walker, and Kenny Q. Zhu.  Princeton Technical Report TR-889-10.  December 2010. (tr, pdf)

Yarra:  An Extension to C for Data Integrity and Partial Safety. Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker and Ben Zorn. Microsoft Technical Report MSR-TR-2010-158. December 2010. (tr)

Frenetic: A High-Level Language for OpenFlow Networks.  Nate Foster, Rob Harrison, Matthew L. Meola, Michael J. Freedman, Jennifer Rexford and David Walker.  Workshop on Programmable Routers for Extensible Services of Tomorrow (PRESTO).  November 2010. (pdf)

Concurrent Separation Logic for Pipelined Parallelization.  Christian J. Bell, Andrew Appel and David Walker.  The 17th Annual Static Analysis Symposium.  September 2010. (pdf)

A Context-free Markup Language for Semi-structured Text. Qian Xi and David Walker.  ACM SIGPLAN Conference on Programming Language Design and Implementation.  June 2010. (pdf)

Ad Hoc Data:  From Uggh to Smug.  David Walker.  International Workshop on Relations and Data Integrity Constraints and Languages. May 2010.  (ppt)

Faulty Logic:  Reasoning About Fault-tolerant Programs.  Matthew Meola and David Walker. European Symposium on Programming.  March 2010.  (pdf)

Semantics and Algorithms for Data-dependent Grammars.  Trevor Jim, Yitzhak Mandelbaum and David Walker.  ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.  January 2010. (ACM digital library) (technical report: pdf)

The Next 700 Data Description Languages. Kathleen Fisher, Yitzhak Mandelbaum, David Walker. Journal of the ACM.  Volume 57, Issue 2, January 2010.  (ACM digital library)

[2009]

An Overview of the Oregon Programming Languages Summer School.  Jim Allen, Zena Ariola, Pierre-Louis Curien, Matthew Fluet, Jeff Foster, Dan Grossman, Robert Harper, Hugo Herbelin, Yannis Smaragdakis, David Walker and Steve Zdancewic.  SIGPLAN Notices, Vol. 44, No. 11. November 2009. (ACM digital library)

Incremental Learning of System Log Formats.  Kathleen Fisher, David Walker and Kenny Q. Zhu. Workshop on the Analysis of System Logs. October 2009. (pdf)

Language Support for Processing Distributed Ad Hoc Data.  Kenny Q. Zhu, Daniel S. Dantas, Kathleen Fisher, Limin Jia, Yitzhak Mandelbaum, Vivek Pai and David Walker. ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, September 2009. (pdf) (technical report TR-826-08: pdf)

Composing Expressive Run-time Security Policies.  Lujo Bauer, Jay Ligatti, and David Walker.  ACM Transactions on Software Engineering and Methodology, Volume 18, Issue 3, pp 9:1-9:43, May 2009. (ACM digital library)

Run-time Enforcement of Nonsafety Policies. Jay Ligatti, Lujo Bauer, and David Walker. ACM Transactions on Information and System Security, Volume 12, Issue 3, pp 1-41, January 2009.  (ACM digital library)

Ad Hoc Data and the Token Ambiguity Problem.  Qian Xi, Kathleen Fisher, Kenny Q. Zhu, and David Walker.  ACM Symposium on Practical Applications of Declarative Languages. January 2009.  (pdf)

[2008]

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

Reasoning About Faulty Programs.  Matthew Meola, Frances Perry and David Walker. Second International Workshop on Proof-Carrying Code.  June 2008.

Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks
Christian Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel and David Walker.  Second International Workshop on Proof-Carrying Code.  June 2008.

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

AspectML: A Polymorphic Aspect-oriented Functional Programming Language.  Daniel S. Dantas, David Walker, Geoffrey Washburn, Stephanie Weirich.   ACM Transactions on Programming Languages and Systems, Volume 30, Issue 3, pp 14:1-14:60, May 2008. (ACM digital library)

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]

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)

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)  Extended report archived as Princeton Technical Report number TR-776-07.  April 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)

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)

[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. (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 ProgramsIMLA 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)

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

Summer School on Foundations of Security.  Invited speaker. June, 03. (PCCppt; TALps)

Poly stop a hacker.  David Walker.  Invited talk, New Jersey Programming Languages Seminar (NJPLS).  September, 02.  (ppt

More Enforceable Security Policies.  A talk at the workshop on Computer Security Foundations.  July 02. (ppt)

Symposium on Cyber Security and Trustworthy Software. Invited speaker. March, 02.  (ppt

 

Major Funding Awards

TC: Large: Collaborative Research: High-Level Language Support for Trustworthy Networks.  NSF CNS-1111520 (PI). $1.4 million.  Received August 2011.

SI2-SSI: Accelerating the Pace of Research through Implicitly Parallel Programming.  NSF OCI-1047879 (Co-PI).  $1.7 million.  Received October 2010.

SHF:Small:Language Support for Ad Hoc Data Processing. NSF award CCF-1016937 (PI). $500,000.  Received August 2010.

Networks Opposing Botnets (NoBot).  ONR award 552404 (Prime ONR N00014-09-1-0770).  (Co-PI).  $400,000. Received April 2009.

Well-typed, Trustworthy Computing in the Presence of Transient Faults. NSF award CNS-0627650 (PI).  $1.1 million. Received August 06.

Language Support for Data-centric Systems Monitoring.  NSF award CNS 0615062 (PI).  $798,975.  Received July 06.

Automatic Tool Generation for Ad Hoc Scientific Data.  NSF award IIS 0612147 (PI).  $493,124.  Received July 06.

Collaborative Research: CSR-PDOS: Managing OS Extensibilty via Aspect-oriented Programming Technology.  NSF award CSR 0615213 (Co-PI).  $315,319.  Received July 06.

Alfred P. Sloan Fellowship.  Received Sept. 04.

Assurance-carrying Components.  ARDA award NBCHC030106 (Co-PI).  Received Oct. 03.

CAREER:  Programming Languages for Secure and Reliable Computing.   NSF award CCF 0238328  (PI).  $437,700.00.  Received March 03.

Scaling Proof-Carrying Code to Production Compilers and Security Policies.  DARPA contract F30602-99-1-0519 (Co-PI).  Received Dec. 02.

Collaborative Research:  High-Assurance Common Language Runtime.  NSF CCR-0208601 (Co-PI).  Received July 02.