Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    text
    copied!<p>Since you explicitly asked for the most interesting and obscure ones:</p> <p>You can extend C-H to many interesting logics and formulations of logics to obtain a really wide variety of correspondences. Here I've tried to focus on some of the more interesting ones rather than on the obscure, plus a couple of fundamental ones that haven't come up yet.</p> <pre><code>evaluation | proof normalisation/cut-elimination variable | assumption S K combinators | axiomatic formulation of logic pattern matching | left-sequent rules subtyping | implicit entailment (not reflected in expressions) intersection types | implicit conjunction union types | implicit disjunction open code | temporal next closed code | necessity effects | possibility reachable state | possible world monadic metalanguage | lax logic non-termination | truth in an unobservable possible world distributed programs | modal logic S5/Hybrid logic meta variables | modal assumptions explicit substitutions | contextual modal necessity pi-calculus | linear logic </code></pre> <p>EDIT: A reference I'd recommend to anyone interested in learning more about extensions of C-H:</p> <p>"A Judgmental Reconstruction of Modal Logic" <a href="http://www.cs.cmu.edu/~fp/papers/mscs00.pdf" rel="noreferrer">http://www.cs.cmu.edu/~fp/papers/mscs00.pdf</a> - this is a great place to start because it starts from first principles and much of it is aimed to be accessible to non-logicians/language theorists. (I'm the second author though, so I'm biased.)</p>
 

Querying!

 
Guidance

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload