Polarity and the Logic of Delimited Continuations

9 years 1 months ago
Polarity and the Logic of Delimited Continuations
Abstract—Polarized logic is the logic of values and continuations, and their interaction through continuation-passing style. The main limitations of this logic are the limitations of CPS: that continuations cannot be composed, and that programs are fully sequentialized. Delimited control operators were invented in response to the limitations of classical continuation-passing. That suggests the question: what is the logic of delimited continuations? We offer a simple account of delimited control, through a natural generalization of the classical notion of polarity. This amounts to breaking the perfect symmetry between positive and negative polarity in the following way: answer types are positive. Despite this asymmetry, we retain all of the classical polarized connectives, and can explain “intuitionistic polarity” (e.g., in systems like CBPV) as a restriction on the use of connectives, i.e., as a logical fragment. Our analysis complements and generalizes existing accounts of deli...
Noam Zeilberger
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LICS
Authors Noam Zeilberger
Comments (0)