The long slow arc of Figurin' Out Things About Focusing continues. I think I found a variant of the token-passing translation of focusing into linear logic, which is a translation of focusing into actually ordered logic, so that, if it works, it means that the asynchronous context really is just an ordinary, legitimate ordered context. Also it has only one token, instead of the proliferation of (destination-passing-y) tokens the linear logic target language requires. The funny novelty that it depends on is getting the why-not modality "?" to properly split into some kind of U and F adjunction. I am not sure this bit actually does work, but I've been poking at it.
The long slow arc of Figurin' Out Things About Focusing continues. I think I found a variant of the token-passing translation of focusing into linear logic, which is a translation of focusing into actually ordered logic, so that, if it works, it means that the asynchronous context really is just an ordinary, legitimate ordered context. Also it has only one token, instead of the proliferation of (destination-passing-y) tokens the linear logic target language requires. The funny novelty that it depends on is getting the why-not modality "?" to properly split into some kind of U and F adjunction. I am not sure this bit actually does work, but I've been poking at it.
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
