User loginNavigation 
From shift and reset to polarized linear logic
By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chungchieh Shan will be interesting to many who loves logic and CurryHoward isomorphism.
From shift and reset to polarized linear logic Abstract: Griffin pointed out that, just as the pure lambdacalculus corresponds to intuitionistic logic, a lambdacalculus with firstclass continuations corresponds to classical logic. We study how firstclass delimited continuations, in the form of Danvy and Filinskiâ€™s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinskiâ€™s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuationpassingstyle (CPS) transform: any pure lambdaterm with an appropriate type is betaetaequivalent to the CPS transform of some shiftreset expression. We conclude that the lambdacalculus with shift and reset and the pure lambdacalculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambdacalculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambdaÂµcalculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in callbyvalue and callbyname settings. By Andris Birkmanis at 20050606 19:17  Functional  Lambda Calculus  Semantics  Type Theory  other blogs  9012 reads

Browse archivesActive forum topicsNew forum topics

Recent comments
4 hours 7 min ago
5 hours 26 min ago
5 hours 48 min ago
9 hours 19 min ago
15 hours 11 min ago
15 hours 18 min ago
17 hours 12 min ago
1 day 2 hours ago
1 day 22 hours ago
2 days 8 hours ago