Prof. Dr. Greg Morrisett

"Ynot: integrating effects with dependent types"

(Vortrag im Rahmen der "Distinguished Lecture Series 07/08" des Max Planck Instituts für Software-Systeme)

I want a type system that will let me capture anything from simple type-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, code, and proofs so that abstraction is feasible.

It turns out that Coq (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, continuations, I/O, etc. For the past year or two, we've been figuring out how to 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 (mildly) interesting code that leverages these features, including thing like hash-tables 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, Lars Birkedal, Rasmus Petersen, Paul Govereau, Avi Shinnar, and Ryan Wisnesky.

Greg Morrisett

Greg Morrisett is the Allen B. Cutting Professor of Computer Science and Associate Dean for Computer Science and Engineering at Harvard University. He received his BS in Mathematics and Computer Science from the University of Richmond in 1989, and his Ph.D. from Carnegie Mellon in 1995. In 1996, he joined the faculty of Cornell University. In the 2003-04 academic year, he took a sabbatical and visited the Microsoft European Research Laboratory, and in 2004, he moved to Harvard.

Morrisett's research has focused on programming languages and software security. He is best known for his work on developing type systems that guarantee strong safety and security properties for low-level languages, including typed intermediate compiler languages, typed assembly language, and Cyclone, a type-safe dialect of C. He received a number of awards for this work, 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.