title: What are the most interesting equivalences arising from the Curry-Howard Isomorphism?
body: <p>I came upon the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="noreferrer">Curry-Howard Isomorphism</a> relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept there exists a precise analogue in formal logic, and vice versa. Here's a "basic" list of such analogies, off the top of my head:</p>
  
  <pre><code>program/definition        | proof
  type/declaration          | proposition
  inhabited type            | theorem/lemma
  function                  | implication
  function argument         | hypothesis/antecedent
  function result           | conclusion/consequent
  function application      | modus ponens
  recursion                 | induction
  identity function         | tautology
  non-terminating function  | absurdity/contradiction
  tuple                     | conjunction (and)
  disjoint union            | disjunction (or)          -- corrected by Antal S-Z
  parametric polymorphism   | universal quantification
  </code></pre>
  
  <p>So, to my question: <strong>what are some of the more interesting/obscure implications of this isomorphism?</strong> I'm no logician so I'm sure I've only scratched the surface with this list.</p>
  
  <p>For example, here are some programming notions for which I'm unaware of pithy names in logic:</p>
  
  <pre><code>currying                  | "((a &amp; b) =&gt; c) iff (a =&gt; (b =&gt; c))"
  scope                     | "known theory + hypotheses"
  </code></pre>
  
  <p>And here are some logical concepts which I haven't quite pinned down in programming terms:</p>
  
  <pre><code>primitive type?           | axiom
  set of valid programs?    | theory
  </code></pre>
  
  <p>Edit:</p>
  
  <p>Here are some more equivalences collected from the responses:</p>
  
  <pre><code>function composition      | syllogism                -- from Apocalisp
  continuation-passing      | double negation          -- from camccann
  </code></pre>