[解決済み] Curry-Howard Isomorphismから生じる最も興味深い同値性とは？

質問

私は カレー・ハワード同型 を知ったのは、私のプログラミング人生の中では比較的遅かったのですが、おそらくこのことが、私がこの概念にすっかり魅了された一因となっているのでしょう。これは、あらゆるプログラミングの概念に対して、形式論理における正確な類似性が存在し、その逆もまた然りであることを意味しています。以下は、私の頭の中にある、そのような類縁関係の基本的なリストです。

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

では、私の質問に この同型性には、どのような興味深い、あるいは不明瞭な意味があるのでしょうか？ 私は論理学者ではないので、このリストは表面を削ったに過ぎないと思います。

たとえば、私が論理学での簡潔な名前を知らないプログラミングの概念がいくつかあります。

currying                  | "((a & b) => c) iff (a => (b => c))"
scope                     | "known theory + hypotheses"

そして、私がまだプログラミング用語としてピンときていない論理的な概念をいくつか紹介します。

primitive type?           | axiom
set of valid programs?    | theory

編集する

以下は、回答から集めた同値の数々です。

function composition      | syllogism                -- from Apocalisp
continuation-passing      | double negation          -- from camccann

どのように解決するのですか？

あなたが最も興味深く、無名のものを明確に尋ねたので。

C-Hを多くの興味深い論理や論理の定式化に拡張して、実に様々な対応関係を得ることができます。 ここでは、曖昧なものよりも、より興味深いもの、さらにまだ出てきていない基本的なものに焦点を当てようとしました。

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

EDIT: C-Hの拡張についてもっと知りたいと思う人にお勧めの参考文献です。

モーダル論理の判断的再構築(邦訳) http://www.cs.cmu.edu/~fp/papers/mscs00.pdf - この本は、第一原理から始まり、その多くが論理学者や言語理論家でない人にもアクセスできることを目的としているので、始めるには最適な場所です。 (私は二番目の著者なので、偏見がありますが）。