My research concerns the theory, design, and implementation of modern programming languages. More specifically, I investigate strongly typed languages such as Java and the Java virtual machine and their application in compilation and security. I use types to direct compiler optimizations, to help ensure compiler correctness, and to check invariants that are required by security systems.

In order to maximize the advantages of compiling with types, I study techniques for propagating type information through the entire compilation process, beyond the level of traditional intermediate languages or bytecodes. To this end, I have designed very low-level languages that expose data structure representations and machine-level operations, yet remain type-safe. The type systems of these languages are powerful enough to encode high-level abstractions such as function closures and abstract data types, but flexible enough to admit most conventional compiler backend optimizations. I am also interested in applying type theory, logic, and other formal methods to concurrent programming, security, and software engineering problems.

Under the guidance of Greg Morrisett, I have investigated the type-directed compilation of advanced languages such as ML and a type-safe variant of C. I have helped design strongly-typed compiler intermediate languages and a type-safe assembly language based on the Intel pentium architecture for the TALC compiler project at Cornell. I am currently investigating ways to extend the theory and implementation of the system to automatically check more sophisticated properties than are implied by conventional type systems. For example, I am studying systems that can ensure resources such as memory or mutual exclusion locks are acquired and released correctly. I have also done work on verifying that programs obey expressive security policies including access control policies and resource bounds policies.

• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In Transactions on Systems and Programming Languages, 21(3):528-569, May 1999.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based Typed Assembly Language. Submitted to the Journal of Functional Programming.

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

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

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

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

• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In the Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85-97, San Diego, Jan. 1998.

• A Type System for Expressive Security Policies at the 1999 Workshop on Run-time Result Verification in Trento, Italy.
• Typed Memory Memory Management in a Calculus of Capabilities at the 1999 Symposium on Principles of Programming Languages in San Antonio, TX.
• Stack-Based Typed Assembly Language at the 1998 Workshop on Types in Compilation in Kyoto, Japan.

• Instructor: Introductory C Programming (100 level). Fall ‘97
• Cornell Computer Science Outstanding TA Award. May ‘96
• Teaching Assistant: Software Engineering (500 level). Fall ’96
• Teaching Assistant: Computers and Programming (200 level). Spring ’96 Fall ’95.

• Referee for the ACM SIGPLAN Workshop on Foundations of Object-Oriented Languages , 2000.
• Referee for the ACM SIGPLAN International Conference on Functional Programming , 1999.
• Referee for the ACM SIGPLAN Conference on Programming Language Design and Implementation, 1999.
• Referee for the ML Workshop , 1998.

• Cornell University: Ph.D. candidate in Computer Science, Fall ’95 – Present.
  • GPA: 4.0
  • Minor field: English Literature
• Queen’s University, Kingston, ON: B.Sc. (Hon.) ’95, Computer Science
  • Prince of Wales Prize, Honorable Mention ’95 (2^nd highest standing in faculty of Arts and Science, Queen’s University)
  • R. W. Leonard Penultimate Year Scholarship ‘94 (highest standing through 3 years of B.Sc., Queen’s University)

• Kandalore Camp (Summer 91-93, 95, 96)
  • Organized and lead a 27-day white-water canoe trip in Northern Quebec, Canada in July-August ’96. Responsible for a group of 16- and 17-year-olds living in isolated Canadian wilderness.
  • Trip Director, June-August ’95. Oversaw more than 50 canoe and kayaking trips. Managed staff, equipment, and transportation.
• Research Assistant, University of Toronto (Summer 94)
  • Studied and evaluated network protocols under Mart Molle
• Kandalore Outdoor Education Center (May-June 92, 93)
  • Taught leadership and communication skills to groups of school childern aged 11-15 in an outdoor environment.

• Wilderness watersports: whitewater canoeing and kayaking, extreme canoe tripping.
• Cityscape sports: hockey, basketball and ultimate frisbee.
• Sedentary sports: bridge, rooting for the Toronto Maple Leafs.

• Greg Morrisett, Assistant Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  jgm@cs.cornell.edu

• Dexter Kozen, Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  kozen@cs.cornell.edu

• Bob Constable, Professor
  Computer Science Dept., Cornell University
  Ithaca, NY 14853
  rc@cs.cornell.edu