title: How can I interpret the typing rules on this paper?
body: <p>Those typing rules are present on the <a href="http://www.sciencedirect.com/science/article/pii/S0890540114001369" rel="nofollow noreferrer">"On the expressivity of elementary linear logic: characterizing Ptime and an exponential time hierarchy"</a> paper:</p>
  
  <p><a href="https://i.stack.imgur.com/GLi1x.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/GLi1x.png" alt="typing rules"></a> </p>
  
  <p>From the <a href="https://stackoverflow.com/questions/12532552/what-part-of-milner-hindley-do-you-not-understand">“What part of Milner-Hindley do you not understand?”</a> Stack Overflow question, I can read some of those in English, but it is still difficult to figure out how to make a type checker out of that. This is my attempt at reading the first 4 rules:</p>
  
  <ul>
  <li><p><strong>Ax</strong>: as an axiom, if x has type A, then x has type A. <em>(Isn't that obvious?)</em></p></li>
  <li><p><strong>Cut</strong>: If a context <code>Γ</code> proves <code>t has type A</code>, and another context <code>∆</code>, extended with the assertion <code>x has type A</code>, proves <code>u has type B</code>, then those two contexts together prove the substitution of all occurrences of <code>x</code> by <code>t</code> in <code>u</code> has type <code>B</code>. <em>(What does that mean, though? Why there are two contexts, where the extra one comes from? Also, that seems like a rule for substitution, but how, if substitution isn't a term, but an operation? The classical Milner-Hindley has nothing like that; it has just a very simple rule for App.)</em></p></li>
  <li><p><strong>Weak</strong>: If a context proves <code>t has type A</code>, then that context extended with the statement <code>x has type B</code> still proves <code>t has type A</code>. <em>(Again, isn't that obvious?)</em></p></li>
  <li><p><strong>Contr</strong>: if a context extended with <code>x1 has type !A</code> and <code>x2 has type !A</code> proves <code>t has type B</code>, then that context, extended with <code>x has type !A</code> proves substituting all occurrences of <code>x1</code> and <code>x2</code> by <code>x</code> in <code>t</code> has type <code>B</code>. <em>(Another rule for substitution, it seems? But why there are two terms above, one term below? Also, why those <code>!</code>s? Where would that all show up on the type checker?)</em></p></li>
  </ul>
  
  <p>I quite get what those rules want to say, but I am missing something before it truly clicks and I'm able to implement the corresponding type checker. How can I approach understanding those rules?</p>