[Colloquium] FW: [TTIC Colloquium] Guest Speaker Announcement

[Ponda Barnes]

Guest Speaker
 
Presented by: Toyota Technological Institute at Chicago
 
Speaker: Aleksandar Nanevski
Speaker's home page:  http://www.eecs.harvard.edu/~aleks
 
Date: Wednesday, May 9, 2007
Time: 10:00 
Location: TTI-C Conference room
 
 
Title: Towards a language design for modular software verification
 
Abstract:
 
In this talk, I will explore some choices that arise if one wants to design
a programming language from scratch, with the intention of supporting
software verification.
 
I will describe Hoare Type Theory (HTT) which integrates a dependently typed
higher-order language, with Hoare-like specifications for reasoning about
mutable state and pointer aliasing. The lack of this integration in the past
has arguably been one of the most significant obstacles in the application
of Hoare-style verification methodology, since it prevented effective
reasoning about constructs for data abstraction, information hiding, and
code reuse.
 
 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, which have so far largely existed in isolation, like Dijkstra's
predicate transformers, Curry-Howard isomorphism, monads, as well as the
more recent idea of Separation Logic.
 
We have formally proved that HTT is modular, in the sense that the
verification of individual program components suffices to establish the
correctness of the whole program. HTT is also (almost) conservative over the
programming practice in modern functional languages; if the verification
features are not used, HTT very much looks like core Haskell.
 
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, and the options for automation of analysis and
reasoning about HTT programs.  
 
 
 
If you have any questions or would like to meet the speaker, please contact
Ponda Barnes at pondabarnes at tti-c.org
For future TTI-C talks and events please go to
http://ttic.uchicago.edu/cal/month.php
 
 
 
 
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20070508/46380320/attachment-0001.html 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: ATT00018.txt
Url: http://mailman.cs.uchicago.edu/pipermail/colloquium/attachments/20070508/46380320/attachment-0001.txt