Paper: Focusing on Binding and Computation (at LICS 2008)

Authors: Daniel R. Licata Noam Zeilberger Robert Harper

Abstract

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 ofimplication, 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 otherhand, 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.

BibTeX

  @InProceedings{LicataZeilbergerHar-FocusingonBindingan,
    author = 	 {Daniel R. Licata and Noam Zeilberger and Robert Harper},
    title = 	 {Focusing on Binding and Computation},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {241--252},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }