Computer Science Dept.
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, P.A. 15213-3891
Office: 7112 Wean Hall
Phone: (412) 268-6714
Starting February 2002, I will be an assistant professor in the
Computer Science Department
at Princeton University. If you have
questions about the future of programming languages at Princeton,
please let me know -- it is sure to be exciting.
I will be unavailable between November 13th and December 9th, 2001.
I will attempt to process email for that time
period during the week following my return.
In case of personal emergencies, please contact my parents
in Toronto at (416) 481-9145.
I study the design, implementation and theory of programming languages.
I am particularly interested in finding new ways to use
type systems and logics to help programmers
write more reliable and secure code.
A significant portion of my tenure as a Ph.D. student
at Cornell University was spent working with
and others on the design and implemention of
a type system for the Intel Pentium processor
Like Java applets, TAL programs (ie: binaries containing
Pentium machine code
and associated typing annotations) may be downloaded
by untrusting clients and checked for safety.
TAL has a firm theoretical foundation and a variety of
practical tools that allow us to compile programs written in a safe
variant of C and to verify the output.
One of the main challenges in the design
of strongly typed low-level languages
is the development of a safe, yet flexible memory model.
Safe languages normally present a highly simplified and restrictive
memory model to the programmer and as a result,
programmers (or compilers, if their output
is a type safe language such as TAL or JVM bytecode) cannot implement their own
optimized, application-specific memory management.
I address this problem by developing a family of type systems
that control aliasing and check the safety of programs
containing explicit initialization, deallocation
and reuse of memory.
The TAL type checker uses one of these type systems to reason about
aliasing in assembly language programs.
I am now a post-doc at Carnegie Mellon University,
working with the FOX Project
groups on advanced programming language technology for systems software. With
Iliano Cervesato and
I am investigating new ways to use
formal logic, logical frameworks
and programming language technology
to aid in the specification of security protocols
and verification of their implementations.
With Bob Harper
and Kevin Watkins,
I am investigating modular and compositional reasoning
I also continue to collaborate with Dan Grossman, Greg Morrisett and Trevor Jim
at Cornell on memory management issues for a new type-safe
variant of C called Cyclone.
Research Publications and Slides from Selected Talks
Curriculum Vitae (Last Updated December 2000)
- Program committee,
ACM SIGPLAN Workshop on Partial Evaluation and
Semantics-based Program Manipulation (PEPM),
Portland, Oregon, Jan. 14-15, 2002.
In association with the Symposium on Principles of Programming Languages
(POPL '02). Please submit a paper!
ACM state-of-the-art summer school on Foundations of Internet Security,
Duszniki Zdrój, Poland, postponed due to the tragic events of
September, 2001. I will be
giving a series of lectures on type systems for safe mobile code
with a focus on the theoretical development of Typed Assembly Language.
For a preview, see my slides on TAL.
They represent the broadest description of what goes into
Typed Assembly Language that is available at an introductory level.
Other topics taught at the school range from Java security
to cryptography to formal analysis of authentication protocols
to intrusion detection.
- Foundations of Language-based Security. Spring, 2002. Princeton.
given in John Reynolds
course on reasoning about low-level programs.
CS 113: C Programming(Instructor, Fall '97)
- Cornell Computer Science Outstanding TA Award(May, '97)
- CS 501: Software Engineering(Teaching Assistant, Fall '96)
- CS 211: Computers and Programming(Teaching Assistant, Fall '95, Spring '96)
- I am a firm believer everyone should do a little whitewater kayaking
every now and then.
Everything I've learned about this sport and about surviving in
the outdoors in general, I learned
- My other outdoor passion is canoe tripping. Two summers ago I did a
month-long trip down the Mistassibi and when I was a teenager,
I did the Missinaibi from Dog Lake to Moosonee. In the summer
of '98 I got back there to do a 10-day trip along the section
from Missinaibi Lake to Mattice. I've also
traveled the Dumoine, Spanish, Magnetewan, and
Petawawa Rivers, among others in Quebec and Ontario.
I'd love to get out to the Nahanni, Copper Mine, or (more realistically)
the Moisie but it is getting harder and harder to find the time ...
- When I'm not exploring the unknown wilds (ie: most of the time),
I satisfy myself while a little old-fashioned shinny (hockey),
the occasional trip to the ski slopes, or a little bridge.
I've also picked ultimate (frisbee) recently.
Quote of the Month (changed semi-annually)
It's hockey season again: Go Leafs go!