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.

What are the right abstractions for programming networks?

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 

Frenetic

Concurrent NetCore:  From Policies to Pipelines.  Cole Schlesinger, Michael Greenberg and David Walker.  To appear in the 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.  To appear in the 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. To appear in the ACM SIGCOMM HotSDN Workshop, August 2014.  (pdf)

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

Infinite CacheFlow in Software-defined Networks.  Naga Katta, Omid Alipourfard, Jennifer Rexford, and David Walker.  To appear in the 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.

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

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)

Optimizing the "One Big Switch" Abstraction in Software-Defined Networks.  Nanxi Kang, Zhenming Liu, Jennifer Rexford and David Walker.  ACM CoNext, Dec 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.  ;login Magazine.  38(5):128-134, 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, 2013. (IEEE version)

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)

Frenetic: A High-Level Language for OpenFlow Networks.  Nate Foster, Rob Harrison, Michael J. Freedman, Jennifer Rexford and David Walker.  Draft (subsumes the short paper at PRESTO).  Cornell Technical Report.  Handle:  http://hdl.handle.net/1813/19310 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)

Ad Hoc Data

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)

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)

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)

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)

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)

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)

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)

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. Princeton Technical Report TR-826-08, July 2008. (pdf)

LearnPADS:  Fully Automatic Tool Generation From Ad Hoc Data. Kathleen Fisher, David Walker and Kenny Q. Zhu.  ACM SIGMOD Demo Session.  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)

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

Zap:  Reasoning about Transient Fault Tolerance

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.

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)

Language-based Security

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)

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)

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)

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 Maps.  Shuvendu Lahiri, Shaz Qadeer and David Walker.  ACM SIGPLAN Workshop on Programming Languages meets Program Verification.  January 2011.  (pdf)

Linear Maps.  Shuvendu Lahiri, Shaz Qadeer and David Walker.  Princeton Technical Report TR-884-10.  September 2010. (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)

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

A Survey of the Practice of Computational Science.  Prakash 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)

Concurrent Separation Logic for Pipelined Parallelization.  Christian J. Bell, Andrew Appel and David Walker.  The 17th Annual Static Analysis Symposium.  September 2010. (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)

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)