Tue May 6, 2008, 4:15-5:30, 3400 Boelter Hall

An Ultimate Type System

John Gregory Morrisett
Harvard University

I want a type system that will let me capture anything from simple safety 
properties, to contracts, and even go all the way to full correctness. 
Furthermore, the language should have a uniform way to treat models, 
specifications, types, and code so that abstraction is feasible.

It turns out that the Coq proof development environment (more or less) has 
such a type system.  Unfortunately, it only works on purely functional programs,
where effects of any kind are forbidden, including non-termination, 
mutable state, exceptions, I/O, etc.  For the past year, we've been figuring 
out how to safely add these features to Coq.  There are some really tricky 
semantic issues that we had to solve, and a number of implementation issues 
that we are still working on.  We've now written some interesting code that 
leverages these features, including things like hash-tables, splay-trees, and 
parser combinators.  The interfaces capture (partial) correctness, and 
are designed, in the style of separation logic, with frame properties that 
make reasoning compositional.

Joint work with Aleks Nanevski (Microsoft), Lars Birkedal (ITU Denmark), 
Rasmus Petersen (ITU Denmark), Paul Govereau, and Avi Shinnar (Harvard).


About the speaker:  Greg Morrisett received his BS in Mathematics and 
Computer Science from the University of Richmond in 1989, and his 
Ph.D. from Carnegie Mellon in 1995. From 1996-2002 he was on the 
faculty at Cornell University, and in 2004, he moved to Harvard as 
the Allen B. Cutting Professor of Computer Science, and assumed the 
position of Associate Dean for Computer Science and Engineering in 
September of 2007.

Morrisett's research focuses on programming languages and software security. 
He is best known for his work on developing type systems for 
low-level languages, including typed intermediate compiler languages, 
typed assembly language, and Cyclone, a type-safe dialect of C.

Morrisett has received a number of awards including a Presidential Early 
Career Award for Scientists and Engineers, an NSF Career Award, 
and an Alfred P. Sloan Fellowship.  He served as Chief Editor for 
the Journal of Functional Programming, and as an associate editor 
for ACM Transactions on Programming Languages and Systems and for 
Information Processing Letters.  Morrisett currently serves on the 
DARPA Information Science and Technology Study Group, Microsoft's 
Trusthworthy Computing Academic Advisory Board, a National Academy 
study on software producibility, and the Fortify Technical Advisory Board.

Host: Todd Millstein.