Campus Event Calendar
Event Entry
What and Who
Programming with Hoare Type Theory
Aleksandar Nanevski
Microsoft Research, Cambridge, UK
SWS Colloquium
I am a postdoc researcher at Microsoft Research, Cambridge, working on formal software verification, theorem proving and type theory. Before that, I graduated from University of Skopje, Macedonia, and wrote my dissertation at CMU under Frank Pfenning. Most of my spare time, I spend with my wife Emi, trying to keep our 3-year old daughter Kalina happy.
AG 1, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 14 April 2009
16:00
60 Minutes
E1 4
019
Saarbrücken
Abstract
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.
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.
Contact
Bettina Bennett
0631-9303-9602
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
204/206
passcode not visible
logged in users only
Bettina Peden-Bennett, 03/26/2009 20:15
Bettina Peden-Bennett, 03/26/2009 14:55 -- Created document.
Bettina Peden-Bennett, 03/26/2009 14:55 -- Created document.