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.

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Daniel R. Licata, Noam Zeilberger, Robert Harper
• Keywords: Computer Science, Inference Rules, LICS 2008, Scoped Inference Rules, Variable Binding