Jason (jcreed) wrote,
Jason
jcreed

I always felt that the main weak point of that bit of research I worked on with Frank back around '07 on intuitionistic letcc (" Intuitionistic letcc via labelled deduction") was the lack of really satisfying examples for why you'd want to have this construct in your programming language.

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...
Tags: linear, logic, modal, transducers
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 4 comments