Copenhagen Programming Language Seminar

Static Contract Checking for Haskell

Dana N. Xu
INRIA, France

Wednesday, June 3, 2009, 15:15-16:00
DIKU North, Universitetsparken 1, Meeting Room A+B (2-0-04)


Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this talk, I will describe a sound and automatic static verification framework for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness. (Published in POPL'09.)

Short Bio: Dana N. Xu received her Ph.D. recently from the University of Cambridge. She now works as a postdoc at INRIA Grenoble in France.

Scientific host:Robert Glück 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