Focusing on Binding and Computation

Add to your list(s) Download to your calendar using vCal

• Dan Licata, Carnegie Mellon University
• Monday 07 September 2009, 14:00-15:00
• UG05 Learning Centre.

If you have a question about this talk, please contact Paul Levy.

Variable binding is a prevalent feature of the syntax and proof theory of many logical systems. In this talk, I will describe 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 {\em 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. The programming language is motivated by Zeilberger’s higher-order focusing for polarized intuitionistic logic, a calculus with strong connections to Levy’s call-by-push-value.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG05 Learning Centre
• computer sience

Note that ex-directory lists are not shown.