University of Birmingham > Talks@bham > Theoretical computer science seminar > Focusing on Binding and Computation

Focusing on Binding and Computation

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

  • UserDan Licata, Carnegie Mellon University
  • ClockMonday 07 September 2009, 14:00-15:00
  • HouseUG05 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.