Focusing on Binding and Computation

10 years 5 months ago
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.
Daniel R. Licata, Noam Zeilberger, Robert Harper
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where LICS
Authors Daniel R. Licata, Noam Zeilberger, Robert Harper
Comments (0)