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

## Focusing on Binding and ComputationAdd 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. |
## Other listsComputer Science Departmental Series Postgraduate Algebra Seminar Physics and Astronomy Colloquia## Other talksProvably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Extending the Lax type operator for finite W-algebras TBC Modelling uncertainty in image analysis. TBC Test talk |