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...

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Noam Zeilberger
• Keywords: Automated Reasoning, Delimited Control Operators, LICS 2010, Linear Logic, Logic