Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Ynot: integrating effects with dependent types
Greg Morrisett
Harvard University
SWS Distinguished Lecture Series - Spring
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 25 March 2008
16:00
60 Minutes
E 1 4
019
MPI SWS Saarbrücken
Abstract
Simultaneous Videocast to MPI, building E1.4, room 019
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.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
Video Broadcast
Yes
University Kaiserslautern
110
24
passcode not visible
logged in users only
Carina Schmitt, 04/07/2008 16:16
Carina Schmitt, 04/03/2008 20:26
Brigitta Hansen, 03/18/2008 14:39 -- Created document.
Carina Schmitt, 04/03/2008 20:26
Brigitta Hansen, 03/18/2008 14:39 -- Created document.