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

                          Mercredi 29 aout, 10h30

                               --------------
                               Andrew Tolmach
                               --------------

                    Portland State University and INRIA

             =================================================
             Proving Properties of Imperative Gallina Programs
             =================================================

I will describe preliminary work on a new approach to proving properties of
simple imperative pointer programs. The basic idea is to represent such
programs via a shallow embedding into a monadic, first-order fragment of the
Coq term language, Gallina. Proofs of program properties can thus be performed
directly on Gallina terms using the full power and flexibility of Coq. In
particular, it is possible to mix reasoning at the level of individual
(monadic) steps with reasoning about the overall effect of larger chunks of
code.

With a little hackery, we can use the existing Coq extraction mechanism to
produce imperative Caml code for our programs. Alternatively, we can define a
deep embedding syntax and operational semantics for our imperative language,
and prove the semantic equivalence of programs expressed at shallow and deep
levels. We anticipate using this latter approach to connect this proof
architecture with the Compcert certified compiler chain.

In this informal talk, I will sketch some examples of proofs in the shallow
embedding, including one for a very simple mark-and-sweep garbage collector.
I'll describe the various approaches for connecting the Gallina code with
concrete executables. Also, I'll briefly contrast this approach with existing
approaches, including those based on VC generation (e.g. Caduceus) and on
direct proofs on the deep embedding (e.g., the work by Appel, Blazy, et al.).