To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 31/01/2003 - 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

                         Vendredi 31 janvier, 10h30

                             ------------------
                             Alberto Momogliano
                             ------------------

                          University of Leicester

                        ===========================
                        An Hybrid Logical Framework
                        ===========================

    Combining Higher  Order Abstract  Syntax (HOAS) and  (co)-induction is
    well known  to be  problematic.  In previous  work [Ambler02]  we have
    described the implementation of  a tool called Hybrid, within Isabelle
    HOL,  which allows  object logics  to be  represented using  HOAS, and
    reasoned  about  using  tactical  theorem proving  and  principles  of
    (co)induction.   Moreover,   it  is  definitional,   which  guarantees
    consistency within a classical type theory.  In this paper we describe
    how to use it in a multi-level reasoning fashion, similar in spirit to
    other meta-logics such FOLDn and  Twelf.  We demonstrate the method by
    formally verifying the  correctness of a compiler for  (a fragment) of
    Mini-ML, following [Hannan92lics].  To further exhibit the flexibility
    of  our  system,  we modify  the  target  language  with a  notion  of
    non-well-founded closure,  inspired by  Milner & Tofte  [Milner91] and
    formally verify via co-induction  a subject reduction theorem for this
    modified language.