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.