But then I started thinking about that transducers paper
chrisamaphone mentioned the other day ("Continuations and Transducer Composition") and realized that it might constitute a legitimate example --- because at least it involves a programming pattern that involves essentially classical linear logic, and the fiddly focusing encodings I've been doing shed some light on how"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...
