Lambda Calculus 歷史年表#
起源期（1920s–1930s）#
| 年份 | 事件 |
|---|---|
| 1928 | Alonzo Church 開始發展 λ 演算，作為研究數學基礎的工具 |
| 1932 | Church 發表以 λ 演算為基礎的邏輯系統（第一篇論文） |
| 1934 | Kleene 證明 λ 可定義函數涵蓋原始遞迴函數 |
| 1935 | Kleene–Rosser 證明 Church 邏輯系統矛盾；Church 轉向純計算部分 |
| 1936 | Church 證明判定問題（Entscheidungsproblem）不可判定；提出 Church 編碼與 Church–Turing 命題；Turing 同年獨立證明，並提出 Turing 機器 |
| 1937 | Turing 證明 λ 可定義函數與 Turing 機器可計算函數等價 |
| 1940 | Church 提出簡單型別 λ 演算，避免邏輯悖論 |
| 1941 | Church 出版《The Calculi of Lambda-Conversion》系統性總結 |
發展期（1940s–1960s）#
| 年份 | 事件 |
|---|---|
| 1958 | John McCarthy 發明 LISP，採用 λ 記法 |
| 1958 | Haskell Curry 出版《Combinatory Logic》，發展組合邏輯 |
| 1963 | Peter Landin 發表 SECD 機器，用 λ 演算解釋 ALGOL 60 |
| 1964 | Landin 提出 ISWIM 語言，影響後世所有函數式語言 |
| 1965 | Curry–Howard 對應由 William Howard 在論文中首次系統化提出 |
| 1969 | Dana Scott 提出 D∞ 模型，建立 λ 演算的語義基礎（domain theory） |
型別理論期（1970s–1980s）#
| 年份 | 事件 |
|---|---|
| 1972 | Jean-Yves Girard 發明 System F（多型 λ 演算） |
| 1972 | Dana Scott 與 Strachey 發展指稱語義（denotational semantics） |
| 1973 | Robin Milner 發明 ML 語言，採用 Hindley–Milner 型別推論 |
| 1974 | John Reynolds 獨立發現多型 λ 演算 |
| 1980 | Per Martin-Löf 發表依賴型別理論（constructive type theory） |
| 1980 | Hindley 出版《Introduction to Combinators and λ-Calculus》 |
| 1985 | Barendregt 出版《The Lambda Calculus: Its Syntax and Semantics》成為標準參考書 |
現代應用期（1990s–至今）#
| 年份 | 事件 |
|---|---|
| 1989 | Coq 證明助手問世（基於 Curry–Howard 對應） |
| 1990 | Haskell 語言誕生（以 Haskell Curry 命名） |
| 2005 | Agda、Idris 等依賴型別語言相繼出現 |
| 2011 | Lean 證明助手問世 |
| 現代 | Python、Java 8、JavaScript、C#、Rust 等主流語言均支援匿名函數（lambda expression） |
關鍵人物年表#
| 年代 | 人物 | 貢獻 |
|---|---|---|
| 1930s | Alonzo Church | 發明 λ 演算 |
| 1936 | Church / Turing | 判定問題不可判定性 |
| 1940 | Church | 簡單型別 λ 演算 |
| 1958 | John McCarthy | LISP |
| 1964 | Peter Landin | SECD 機器、ISWIM |
| 1969 | Dana Scott | Domain theory 語義 |
| 1972 | Jean-Yves Girard | System F |
| 1980s | 多位學者 | Curry–Howard 對應系統化 |
| 1990 | Haskell 委員會 | Haskell 語言 |