![]() |
![]() |
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
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:
Note that ex-directory lists are not shown. |
Other listsNuclear physics seminars Centre for Computational Biology Seminar Series Type the title of a new list hereOther talksHorizontal Mean Curvature Flow and stochastic optimal controls TBA TBA TBA TBA Wave turbulence in the Schrödinger-Helmholtz equation |