But then I started thinking about that transducers paper
"classical linear logic can simulate intuitionistic logic"
and
"classical S4 modal logic can simulate intuitionistic logic"
are doing almost exactly the same thing.
It's worth some more thought...