Curry–Howard対応（Curry–Howard Correspondence）は、論理学・型理論・計算機科学の橋渡しとなる非常に重要な発見です。最初から体系的に提唱されたものではなく、複数の研究者の独立した成果が数十年をかけて構造的に結びついていったという来歴があります。
🕰 来歴：時系列とキーパーソン
| 年代 | 出来事 |
|---|
| 1930年代 | Haskell Curry が「命題論理」と「単純型付きラムダ計算」の類似に着目（証明構造と関数構造の一致） |
| 1940年代 | Curry、Feys によって命題論理と λ計算の対応が明文化される（ただし当時は明示的に対応とは呼ばれていない） |
| 1969年 | William Alvin Howard が論文「The formulae-as-types notion of construction」で、「命題＝型、証明＝項（プログラム）」という構造的な対応を明示化 → 現代的 Curry–Howard対応の誕生 |
| 1970年代 | de Bruijn によって、型理論の形式化（Automath）と形式証明言語の設計が進む |
| 1980年代以降 | Coq、Agda、MLなどの関数型言語で実用化が進み、証明支援系や型推論の根幹理論になる |
| 1990–2000年代 | Curry–Howard対応が**直観主義論理（intuitionistic logic）**との親和性を持つことが確立される |
| 2010年代 | Homotopy Type Theory（HoTT） により、対応関係が空間的構造（パス、ホモトピー）へ拡張される |
👤 各人物の貢献
🧠 Haskell Curry（1900–1982）
- 命題論理をラムダ計算で形式化
- 「関数」と「証明」の形式構造の一致に最初に気づいた先駆者
- → 後に「カリー化（Currying）」と呼ばれる変換の語源にもなる
🧠 William Alvin Howard（1926–）
- 「命題 = 型」という直観的だが深い洞察を1969年に明文化
- 「型の観点からの構成主義」という革新的アイデアを提示
- 彼の論文は当時あまり注目されなかったが、後に計算機科学と数理論理で大きな影響を与える
🧠 Nicolaas de Bruijn（1918–2012）
- 形式証明言語 Automath を設計し、型理論の実装へと進展
- 論理と型の対応を実際のプログラムと証明で結びつける
🧩 対応が発見された背景
1. ラムダ計算の形式的な強さ
- λ計算は、形式的に「関数」「構文木」「推論過程」を記述できるツールだった
2. 直観主義論理と構成主義
- 「証明があるとは、構成できること」という哲学（Brouwer、Heyting）において、
- 「構成＝プログラム」とみなせる構図が浮上
3. 型付き関数型言語の勃興
- ML、Haskellなどの関数型言語が型理論を背景に発展し、
- 「型＝命題」として安全性と検証性を支える仕組みになる
📚 関連文献
- Howard, W. A. (1969). The formulae-as-types notion of construction.
- Curry, H. B., & Feys, R. (1958). Combinatory Logic.
- de Bruijn, N. G. (1970s). Automath papers.
- Sørensen & Urzyczyn. Lectures on the Curry–Howard Isomorphism（教科書として優良）
🔄 その後の展開
- Curry–Howard–Lambek対応：圏論（Category Theory）とも結びつき、構造的意味論（categorical semantics）として拡張
- Curry–Howard–Homotopy対応：HoTTにより空間的意味を持つ型理論へと進化（2010年代以降）
- 形式検証・証明支援系への応用：Coq, Agda, Lean などによりソフトウェアや定理の安全な構成が可能に
✅ まとめ：Curry–Howard対応の来歴
| 時代 | 概要 |
|---|
| 1930年代 | Curry：論理とラムダ計算の対応に着目 |
| 1969年 | Howard：「命題＝型、証明＝項」の明文化 |
| 1970年代 | de Bruijn：型理論をプログラム化（Automath） |
| 1980年代以降 | 証明支援系、関数型言語への応用 |
| 2010年代以降 | HoTTでの空間的拡張、∞-groupoidとの接続 |
