Research stuff is looking peachy keen about now. I swizzled things around from yesterday, and out popped a version that is much more obviously conservative over LLF. I think the worst news I could get right now is to find out something dangerously similar has already been done, which is conceivable. But the simplicity that makes me worried about being original means conversely that I'm very confident now that what I have hangs together as a valid system, rather confident that it'll work for a few examples at least (at least linear cut elimination...) and dreamily optimistic that it might have some interesting connections to BI semantics after all. I have a hard time believing that exactly the same thing has been done before, since it makes heavy use of all this awesome canonicalizing substitution stuff due to Kevin Watkins and friends, and it doesn't seems like that has gained much of a foothold outside CMU yet.
Research stuff is looking peachy keen about now. I swizzled things around from yesterday, and out popped a version that is much more obviously conservative over LLF. I think the worst news I could get right now is to find out something dangerously similar has already been done, which is conceivable. But the simplicity that makes me worried about being original means conversely that I'm very confident now that what I have hangs together as a valid system, rather confident that it'll work for a few examples at least (at least linear cut elimination...) and dreamily optimistic that it might have some interesting connections to BI semantics after all. I have a hard time believing that exactly the same thing has been done before, since it makes heavy use of all this awesome canonicalizing substitution stuff due to Kevin Watkins and friends, and it doesn't seems like that has gained much of a foothold outside CMU yet.
- Post a new comment
- 6 comments
- Post a new comment
- 6 comments
