To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Cristal - 17/12/02 - Paris - FR

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


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                          Mardi 17 decembre, 10h30

                            -------------------
                            Richard B. Kieburtz
                            -------------------

                         Oregon Graduate Institute

         =========================================================
         Programatica -- Certifying properties of Haskell programs
         =========================================================


    Many properties of interest to  users of software systems are not easily
    captured in a comprehensive notion of correctness but are more naturally
    expressed as  specific safety or  liveness properties.  Software  can be
    certified to have specific functional (as distinguished from behavioral)
    properties on the basis of  evidence that can take many different forms,
    including testimony of expert reviewers, systematic testing, state-space
    exploration and  formal proof.  A  certificate is an  authenticated link
    from a  program and a property  asserted of the program  to evidence for
    that property.  The Programatica  project is exploring certification for
    properties  of   Haskell  programs.  Programatica   includes  logic  for
    expressing properties  of Haskell terms, a formal  semantics for Haskell
    and for its logic, a  notion of certificates and certificate management.
    This talk will give an overview of Programatica, its logic, and the role
    of certificate management.