I think I totally nailed down the destination-passing result. I had…: jcreed

I think I totally nailed down the destination-passing result. I had to break symmetry once more --- not only do I have to do a different translation on the left and the right of the turnstile, I also have to have different induction hypotheses for the "forward" and "backward" entailments in the asynchronous part. A bit of a bummer, but at least the proof goes through. Certainly a relief after about 10 hours of continuous pounding away trying to prove a falsehood.

Thanks to

simrob for planting the idea in my head of how incredibly related ordered logic on the one hand and destination-passing in linear logic on the other are. He showed me how moving away from destination passing in structural operational semantics makes your life easier, but I've found for my application that avoiding the ordered context and passing destinations seems better.

(no subject)

(no subject)

(no subject)

Error