|
|
Greg
Morrisett |
| Allen B. Cutting Professor of
Computer Science |
|
| Associate Dean for Computer
Science and Engineering |
|
| School of Engineering and
Applied Sciences |
|
| Harvard
University |
|
| 151 Maxwell Dworkin Hall |
|
| 33 Oxford Street |
|
| Cambridge, MA 02138 |
|
| Phone: (617)
495-9526 Fax: (617) 495-2498 |
|
| Email: greg {at}
eecs.harvard.edu |
My administrative assistant is Tristen Hubbard, Maxwell Dworkin 239, (617) 496-7358, tristen at eecs.harvard.edu.
My current research interests are in the applications of programming language technology for building secure and reliable systems. In particular, I am interested in applications of advanced type systems, model checkers, certifying compilers, proof-carrying code, and inlined reference monitors for building efficient and provably secure systems. I am also interested in the design and application of high-level languages for new or emerging domains, such as sensor networks.
Research projects:
| The Center for Research on
Computation and Society: The Center for
Research on Computation and Society (CRCS) brings
computer scientists together with a broad range of researchers,
including economists, psychologists, legal scholars, ethicists,
neuroscientists, and other academic colleagues. |
|
| Ynot: A next
generation
functional
programming language that provides clean support for dependent and
refinement types within a modern functional language. The focus
of this work is on the integration of dependent types with effectful computations so that we
can reason as easily about programs with effects as without. |
|
| The
Cyclone Safe-C Project:
Cyclone is a type-safe dialect of C
that
provides good control over data representations and memory management
without sacrificing safety. It uses a combination of novel
technologies,
including region-based types, wrapped libraries, and link-time checking
to achieve these goals. |
|
|
Macroprogramming
Sensors: We are investigating high-level languages for
programming diverse, distributed networks of inexpensive sensors.
Our goal is
to greatly simplify sensor network application design by providing
high-level programming abstractions, and primitives that automatically
compile down to the complex, low-level operations implemented by each
sensor node. |
|
| PittSFIeld:
Stephen McCamant
(MIT) and I developed an efficient software-based fault isolation (SFI)
tool for x86 code. The tool can be used to restrict a process
from reading, writing, or executing addresses outside a specified range
without the need for hardware-based process isolation. |
|
| Typed Assembly Language: A type system for the Intel x86 assembly language. The TAL type system is rich enough that we can efficiently encode a number of high-level language constructs, yet it is still possible to statically verify that the machine code will respect type safety when executed. The latest release (2.0) of the TAL tools can be found here. |