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

                          Lundi 20 octobre, 10h30

                -------------------------------------------
                               Robert Harper
                (joint with Dan Licata and Noam Zeilberger)
                -------------------------------------------

                         Carnegie Mellon University

                    ===================================
                    Focusing on Binding and Computation
                    ===================================

Variable binding is a prevalent feature of the syntax and proof theory of many
logical systems.  In this paper, we define a programming language that
provides intrinsic support for both representing and computing with binding.
This language is extracted as the Curry-Howard interpretation of a focused
sequent calculus with two kinds of implication, of opposite polarity.  The
representational arrow extends systems of definitional reflection with a
notion of scoped inference rules, which are used to represent binding.  On the
other hand, the usual computational arrow classifies recursive functions
defined by pattern-matching.  Unlike many previous approaches, both kinds of
implication are connectives in a single logic, which serves as a rich logical
framework capable of representing inference rules that mix binding and
computation.