Type theory and functional programming: a history

From Frege's Begriffsschrift and Russell's theory of types to the lambda calculus, Curry–Howard, ML and Haskell, dependent types and proof assistants, and functional ideas in mainstream languages. Moments are tagged (type theory, logic, lambda calculus, category theory, proof assistants, languages, compilers & implementation, effects, people) and colored by their first tag; eras are shown as spans and lines trace lineages. Dates are publication or release dates unless a note says otherwise. Summaries are our own; each moment links to its Wikipedia sources.

82 moments · 1879-01-01T00:00:00Z CE – 2025-01-01T00:00:00Z CE · by @athan · @athan

Moments

1. Frege's Begriffsschrift 1879-01-01T00:00:00Z CE
2. Russell writes to Frege about his paradox 1902-06-16T00:00:00Z CE
3. Russell's theory of types 1908-01-01T00:00:00Z CE
4. Principia Mathematica 1910-01-01T00:00:00Z CE
5. Schönfinkel's combinators 1924-01-01T00:00:00Z CE
6. Curry's combinatory logic 1930-01-01T00:00:00Z CE
7. Church introduces the lambda calculus 1932-01-01T00:00:00Z CE
8. Curry notices formulas are types 1934-01-01T00:00:00Z CE
9. The Kleene–Rosser paradox 1935-01-01T00:00:00Z CE
10. Church and Turing: computability 1936-01-01T00:00:00Z CE
11. Church's simple theory of types 1940-01-01T00:00:00Z CE
12. Category theory 1945-01-01T00:00:00Z CE
13. Combinatory Logic, volume I 1958-01-01T00:00:00Z CE
14. LISP 1958-01-01T00:00:00Z CE
15. "Recursive Functions of Symbolic Expressions" 1960-04-01T00:00:00Z CE
16. Lawvere's functorial semantics 1963-01-01T00:00:00Z CE
17. Landin's SECD machine 1964-01-01T00:00:00Z CE
18. ISWIM: "The Next 700 Programming Languages" 1966-03-01T00:00:00Z CE
19. Automath 1967-01-01T00:00:00Z CE
20. Hindley's principal type schemes 1969-01-01T00:00:00Z CE
21. Howard's "formulae-as-types" 1969-01-01T00:00:00Z CE
22. Scott's domain theory 1969-01-01T00:00:00Z CE
23. Girard's System F 1972-01-01T00:00:00Z CE
24. Girard's paradox 1972-01-01T00:00:00Z CE
25. Cartesian closed categories 1972-01-01T00:00:00Z CE
26. LCF 1972-01-01T00:00:00Z CE
27. Martin-Löf type theory 1972-01-01T00:00:00Z CE
28. SASL 1972-01-01T00:00:00Z CE
29. ML 1973-01-01T00:00:00Z CE
30. Reynolds's polymorphic lambda calculus 1974-01-01T00:00:00Z CE
31. Scheme 1975-01-01T00:00:00Z CE
32. Backus's Turing Award lecture 1977-10-01T00:00:00Z CE
33. "A Theory of Type Polymorphism in Programming" 1978-01-01T00:00:00Z CE
34. Hope 1980-01-01T00:00:00Z CE
35. Howard's paper is published 1980-01-01T00:00:00Z CE
36. KRC 1981-01-01T00:00:00Z CE
37. Damas–Milner 1982-01-01T00:00:00Z CE
38. Nuprl 1984-01-01T00:00:00Z CE
39. The Calculus of Constructions 1985-01-01T00:00:00Z CE
40. Miranda 1985-01-01T00:00:00Z CE
41. Erlang 1986-01-01T00:00:00Z CE
42. Isabelle 1986-01-01T00:00:00Z CE
43. Linear logic 1987-01-01T00:00:00Z CE
44. The Haskell committee forms 1987-09-01T00:00:00Z CE
45. Coq 1989-01-01T00:00:00Z CE
46. Moggi's monads 1989-01-01T00:00:00Z CE
47. Theorems for free! 1989-01-01T00:00:00Z CE
48. The Definition of Standard ML 1990-01-01T00:00:00Z CE
49. Haskell 1.0 1990-04-01T00:00:00Z CE
50. The lambda cube 1991-01-01T00:00:00Z CE