for all my research is the application of advanced semantic constructs in real-world applications.
Recently, I have concentrated on type systems and logics for enforcing security properties in low-level code. One byproduct of this research is the design of a type system called TAL (Typed Assembly Language) for the Intel x86 architecture and a suite of tools that can efficiently type check binary code. The TAL type system is sufficiently expressive that we can efficiently compile a variety of high-level safe languages, such as ML, Scheme, Safe-C, or Java, to type-correct assembly code. This technology provides a means to safely extend systems such as kernels, web browsers, or hand-helds without the overheads of a virtual machine or just-in-time compiler. Recent work on TAL includes extending the type system to provide enforcement of other security policies, such as resource constraints, that are outside the scope of traditional type systems. I am also studying how other language technologies, such as binary rewriting and inlined reference monitors, can be combined with types and logics to support a wider class of important security properties.
Another interest is in language, compiler, and runtime support for application-specific memory management. Though standard garbage collection techniques provide a safe and convenient programming model, many systems applications cannot tolerate the overheads introduced by a general-purpose collector. My research here focuses on a range of topics from fast conservative garbage collectors, to advanced type systems for region-based memory management, to generalizations of linear type systems. The goal in all of this work is to provide the programmer with more control over memory management without sacrificing safety.
My other recent interests are in run-time code generation and modal type systems, efficient data representation, and rich forms of polymorphism. Many of these issues are being explored in the context of Cyclone, a next-generation systems language that is being developed jointly between researchers at Cornell and AT&T Laboratories.
NSF Faculty Early Career Development Award (1999).
University Activities Member: Ph.D. admissions committee, 1998, 1999.
Editor: Journal of Functional Programming.
Associate Editor: ACM Transactions on Programming Languages and Systems.
Member: IFIP Working Group 2.8 on Functional Programming.
Participant: INFOSEC Research Council Study Group on Malicious Code; DARPA ISAT Study on Mobile Code.
Program Committee Member: Symposium on Principles of Programming Languages (PoPL 2001); International Conference on Functional Programming (ICFP 2000); Principles and Practice of Declarative Programming (PPDP 2000); International Symposium on Memory Management (ISMM 2000).
Mobile Code Security. Air Force Scientific Advisory Board, December 1999.
Advanced Type Systems for Low-Level Languages. OpenSIG Conference, October 1999.
Why Languages and Compilers Matter. INFOSEC Research Council Study Group on Malicious Code, October 1999.
The Role of Type Systems in Mobile Code Security. DARPA ISAT Study Group on Mobile Code, January 2000.
Mobile Code Security: An Overview. TARA Review, Air Force Research Laboratory, March 2000.
“Type Structure for Low-Level Programming Languages.” 1999 International Colloquium on Automata, Languages, and Programming (with K. Crary).
“From System F to Typed Assembly Language.” In ACM Transactions on Programming Languages and Systems, 21(3) (May 1999), 528–569 (with D. Walker, K. Crary, and N. Glew).
“Principals in Programming Languages: A Syntactic Proof Technique.” In the 1999 International Conference on Functional Programming, Paris, France (September 1999), 197–207 (with S. Zdancewic and D. Grossman).
“Alias Types.” European Symposium on Programming, Berlin, Germany (March 2000) (with F. Smith and D. Walker).