To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Cristal - 23/02/05 - Paris - FR

           Vous pouvez 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 conférences du bâtiment 7

                         Mercredi 23 fevrier, 14h00

                                ------------
                                Jaap Boender
                                ------------

                        Radboud University, Nijmegen

          ========================================================
          A tactic for proving primitive recursive formulas in Coq
          ========================================================

We will present a method for automatically proving primitive recursive
formulas. This method makes use of reflection: a theorem is translated
to a representation in an abstract syntax, and then this
representation is reduced to a boolean value. The method is
implemented as a Coq tactic using Ocaml; it can deal with theorems
about natural numbers and integers. Coq is also used to prove the
correctness of the translation and reduction.