skip to main |
skip to sidebar
###
a paper

*Focusing on binding and computation*Dan Licata,

Noam Zeilberger, and

Robert HarperTo appear at

LICS 08

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.

Comments appreciated!

## 1 comment:

Post a Comment