Copenhagen Programming Language Seminar

Programming with Hoare Type Theory

Aleks Nanevski
Microsoft Research, Cambridge

Tuesday 10 March 2009, 13:00-14:00
The IT University, Rued Langgaards Vej 7, DK-2300 Auditorium 4


Two main properties make type systems an effective and scalable formal method. First, important classes of programming errors are eliminated by statically enforcing the correct use of values. Second, types facilitate modular software development by serving as specifications of program components, while hiding the component's actual implementation. Implementations with the same type can be interchanged, thus facilitating software reuse and evolution.

Mainstream type systems focus on specifying relatively simple properties that admit type inference and checking with little or no input from the programmer. Unfortunately, this leaves a number of properties, including data structure invariants and API protocols outside of their reach, and also restricts the practical programming features that can be safely supported. For example, most simply-typed languages cannot safely allow low-level operations such as pointer arithmetic or explicit memory management.

In this talk, I will describe Hoare Type Theory (HTT) which combines dependent types of a system like Coq with features for specification and verification of low-level stateful operations in the style of Hoare and Separation Logic.

Such a combination is desirable for several reasons. On the type-theoretic side, it makes it possible to integrate stateful behaviour into dependent type theories that have so far been purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms of type theory, which are essential for scaling the verification effort.

I will discuss the implementation of HTT, verification of various examples that I have carried out, as well as the possibilities for extending HTT to support further programming features such as concurrency.

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