To: seminaire@pauillac.inria.fr
From: Bruno.Barras@inria.fr
Subject: SEM - INRIA : LogiCal - 11/10/02 - 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 11 octobre, 10h30

                                ------------
                                Jamie Gabbay
                                ------------

                         Cambridge University (UK)

      ================================================================
      Fraenkel-Mostowski: semantics, logics, and languages for binding
      ================================================================


    It  is well-known  that  the framework  of  inductive definitions  can
    interact  poorly  with  variable  binding.  For  example  in  defining
    capture-avoiding substitution  we may  have to rename  bound variables
    and there is no canonical way of doing so.

    FM (Fraenkel-Mostowski)  techniques give a semantics  to binding based
    on  a  novel  mathematical  foundation.   The  resulting  systems  are
    astonishingly nice.

    Applications  of   a  better  handling  of   binding  include  program
    transformation  and compiler  optimisation, operational  semantics and
    models of process calculi  with name generation, logics for describing
    binding  and  their proof  theory,  programming  language design,  and
    theorem-proving systems.


    About  the  speaker: I  am  employed on  the  FreshML  project in  the
    Cambridge Computer Laboratory, UK.  We are developing a compiler based
    on  ML which includes  features for  declaring inductive  datatypes of
    syntax with  binding, designed using  soundness with respect to  an FM
    semantics.