Profile photo for Hunan Rostomyan

Here are some highlights from Dana Scott's list of important events in a not very small branch of mathematical logic called computability theory.

1910s

Principia Mathematica (Whitehead, Russell)

1920s

Lowenheim-Skolem Theorem (Skolem)
Combinators (Schonfinkel, Curry)
NBG set theory (von Neumann, later: Bernays, Godel)
Epsilon calculus (Hilbert, Bernays)
Simple theory of types (Chwistek, Ramsey, Carnap)

1930s

Combinatory logic (Curry)
FOL is complete (Godel)
PA is incomplete (Godel)
Untyped lambda-calculus (Church)
Church-Rosser Theorem (Church, Rosser)
Post-Turing machines (Post, Turing)
Halting problem is undecidable (Church, Turing)

1940s

Lambda calculus (Church)
Category theory (Eilenberg, MacLane)

1950s

FOL is Henkin-complete (Henkin)

1960s

Cartesian closed categories (Eilenberg, Kelly)
Normalization Theorem (Tait)
Dependent types (Howard, de Bruijn)
Typed domain logic (D. Scott)
Curry-Howard Isomorphism (Howard, Curry)

1970s

Categorical logic (Joyal)
Martin-Lof type theory (Martin-Lof)
Polymorphic lambda-calculus (Reynolds)
First-order categorical logic (Makkai, Reyes)

1980s

Calculus of constructions (Coquand, Huet)
Bounded quantification (Cardelli, Wegner)
Higher-order categorical logic (Lambek, P. J. Scott)
Linear logic (Girard)
Computational lambda-calculus (Moggi)

1990s

HIgher-type recursion theory (Sacks)
Lazy lambda-calculus (Abramsky)
Pi-calculus (Milner, Parrow, Walker)
Categorical combinators (Curien)
Algebraic set theory (Joyal, Moerdijk)
Object calculus (Abadi, Cardelli)
Categorification (Baez)

2000s

Predicative topos (Moerdijk, Palmgren)
Differential lambda-calculus (Erhrhard, Regnier)
Homotopy type theory (Awodey, Warren)
Univalence axiom (Voevodsky)


Source: Dana Scott, "Lambda-calculus: then and now", 2012.

View question
About · Careers · Privacy · Terms · Contact · Languages · Your Ad Choices · Press ·
© Quora, Inc. 2025