Jason (jcreed) wrote,

Liang and Miller's upcoming LICS paper Unifying Classical and Intuitionistic Logics for Computational Control is pretty interesting. I think the sequent calculus on page 8 is the fastest way to understand what it's about. Atoms are colored red (intuitionistic) or green (classical). There are two falsehoods, 0 (intuitionistic) and ⊥ (classical). The letter e stands for either a green atom or ⊥. So basically it looks like a multiple-conclusion calculus where implication erases all other conclusions --- except there's this extra cupboard Delta that you can hide whatever you want in, except you can only get stuff out of it if an e appears somewhere on the right of the turnstile.

Meanwhile Bernardy and Moulin's Type-Theory In Color nearly resembles a sigbovik paper and I absolutely mean that in the most complimentary way possible.
Tags: logic, math, modal logic

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded