To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 04/03/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 4 mars, 10h30

                              ---------------
                              Noam Zeilberger
                              ---------------

                         Carnegie Mellon University

               ==============================================
               From AHOS to HOAS (duality for fun AND profit)
               ==============================================

To be, or to do: that is the question.  One of the important lessons
of linear logic is that connectives come in two flavors: *positive*
connectives (like * and +) are in a sense defined by what they are,
*negative* connectives (like & and -o) are defined by what they do.
Computationally, it turns out this distinction is intimately related
to pattern-matching, and can be formalized through "abstract
higher-order syntax" (POPL '08).  After defining the syntax of
*constructor* patterns for positive types (like strict products and
sums), we can define the syntax of continuations for those types
abstractly, as maps from constructor patterns to expressions.  Dually,
we define *destructor* patterns for negative types (like lazy products
and functions), and then define negative values abstractly, as maps
from destructor patterns to expressions.  From a practical
perspective, AHOS has the advantage of being easily encoded in type
theories based on iterated inductive definitions (such as Coq and
Agda2), allowing us to reuse their pattern coverage-checkers.  We can
also prove a modular type safety theorem.

In recent work with Licata and Harper, we extended this analysis to
give a new account of traditional, LF-style higher-order abstract
syntax.  The intuition boils down to this: if it is possible to
pattern-match against a value of higher-order type (e.g., as done by
Twelf), then the function space should be positive.  This lead us to
introduce an unusual, positive *representational arrow*, in addition
to the ordinary, negative *computational arrow*.  I will describe some
of our (preliminary) experience with this new approach to representing
HOAS, and with programming with HOAS encodings using AHOS.