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.
-
(no subject)
A paper on describing circuits in an agda DSL: http://www.staff.science.uu.nl/~swier004/publications/2015-types-draft.pdf
-
(no subject)
Going more carefully now through this little tutorial on fpga programming with the iCEstick. It's in spanish, which makes it slightly more…
-
(no subject)
Some further progress cleaning up the https://xkcd.com/1360/ -esque augean stables that is my hard drive. Tomato chicken I made a couple days ago…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
