When & Where: 12:30pm, Friday, October 27, 2006, Room 200 AKW
Abstract:
Hoare Type Theory (HTT) combines a dependently typed, higher-order language with monadically-encapsulated, stateful computations. The type system incorporates pre- and post-conditions, in a fashion similar to Hoare and Separation Logic, so that programmers can specify the requirements and effects of computations, within types. This integrates programming with specification, and typechecking with verification.
In this talk, I will discuss some benefits of the integration. For example, HTT enables provably modular reasoning in the presence of higher-order functions, polymorphism, abstract types, pointer aliasing, memory allocation and deallocation. It also becomes possible to represent private state of functions or datatypes, and provide fine-grained control over access to and ownership of this state.
Biography:
Aleks Nanevski is a postdoctoral fellow at Harvard University, working with Professor Greg Morrisett. Aleks' research investigates programming languages, type systems and logics that can structure and reason about the interaction of programs with their execution environments.