Copenhagen Programming Language Seminar

Program verification with Hoare Type Theory

Aleks Nanevski
Microsoft Research, Cambridge, UK

Monday, January 21, 2008, 11:00-12:00
ITU, Rued Langgaards Vej 7, Auditorium 4


In this talk, I will describe Hoare Type Theory (HTT) which combines dependent type theory like Coq with features for specification and verification in the style of Hoare Logic.

This combination is desirable for many reasons. On the type-theoretic side, it makes it possible to integrate stateful behaviour into languages and logics that have so far been limited to be purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms, which are essential for scaling any kind of verification effort. On the functional programming side, the language may roughly be considered as a dependently typed extension of core Haskell.

Finally, from the technical standpoint, it is interesting that the design of HTT relates in an essential way some of the most venerable ideas from language theory like Dijkstra's predicate transformers, Curry-Howard isomorphism, monads, as well as the more recent idea of Separation Logic, which have not been connected before.

I will discuss the implementation of HTT (called Y-not) which is currently under way, as well as the possibilities for scaling HTT to support further programming features.

Scientific host: Lars Birkedal. Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org