To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 26/02/08 - 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 26 février, 10h30

                              ----------------
                              Pierre Corbineau
                              ----------------

                        Radboud University Nijmegen

             ==================================================
             A Declarative Language For The Coq Proof Assistant
             ==================================================

We present a new proof language for the Coq proof assistant. This language
uses the declarative style. It aims at providing a simple, natural and robust
alternative to the existing Ltac tactic language. We give the syntax of our
language, an informal description of its commands and its operational
semantics. We explain how this language can be used to implement formal proof
sketches. Finally, we present some extra features we wish to implement in the
future.