To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 03/03/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

                            Mardi 3 mars, 10h30

                                ------------
                                Andrew Gacek
                                ------------

                          University of Minnesota

         =========================================================
         A Framework for Specification, Prototyping, and Reasoning
         =========================================================

This talk focuses on the specification of and reasoning about formal
systems such as type assignment and evaluation semantics in
programming languages. I introduce a logic which allows key aspects of
such systems, including variable binding structure within the objects
they deal with, to be specified directly and which allows reasoning to
be performed over these specifications. Many of these reasoning tasks
inductively analyze the structure of terms by instantiating bound
variables with fresh free variables. I show how this can be captured
in a logical setting through a process of moving binding from the term
level to the proof level. It is often necessary in reasoning to be
able to identify occurrences of variables captured by such proof level
binders and to be able to distinguish between variable occurrences
governed by different binders. I describe a new logical device that is
capable of capturing such rich properties about binding, and I show
how this device can naturally encode informal arguments based on free
variable occurrences.  Stepping back, I show how many similar features
of specifications can be abstracted out by using an intermediate
specification logic. I briefly describe how this intermediate
specification logic can be given an operational semantics so that
specifications can be animated automatically, and I explain how the
specification logic can be exploited during reasoning to yield many
interesting theorems "for free". Finally, I discuss the implementation
of these ideas in the Abella theorem proving system and describe the
applications of it that I have explored thus far.