To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 16/02/09 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Lundi 16 février, 10h30

                                 ----------
                                 Dana N. Xu
                                 ----------

                University of Cambridge & INRIA Rhône-Alpes

                    ====================================
                    Static Contract Checking for Haskell
                    ====================================

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 paper, we 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.