[TYPES] focusing on binding and computation

[Robert Harper]

We are pleased to accounce a technical report on a new approach to
integrating higher-order abstract syntax with a functional programming
language:

  Focusing on Binding and Computation
  Daniel R. Licata, Noam Zeilberger, Robert Harper
  PDF and companion code:
    http://www.cs.cmu.edu/~drl/pubs.html

  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 {\em two} kinds of
  implication, of opposite polarity.  The \emph{representational arrow}
  extends systems of definitional reflection with the notion of a scoped
  inference rule, which permits the adequate representation of binding  
via
  higher-order abstract syntax.  On the other hand, the
  usual \emph{computational arrow} classifies recursive functions over
  such higher-order data.  Unlike many previous approaches, both binding
  and computation can mix freely.  Following Zeilberger [POPL 2008], the
  computational function space admits a form of open-endedness, in  
that it
  is represented by an abstract map from patterns to expressions.  As we
  demonstrate with Coq and Agda implementations, this has the important
  practical benefit that we can reuse the pattern coverage checking of
  these tools.

Comments welcome!
Dan, Noam, and Bob