Reference1
1908 | Bertand Russel2. Invented.
1933 | Alonzo Church3 [^chu40] [^chu41]. Rigorous formal system. Named $\lambda$-calculus.
1998 | Per Martin-Löf[^ML98]. a “predicative” modification of Church’s type system (dependent, constructive, intuitionistic). Named Martin-Löf type theory.
[^ML98] Per Martin-Löf. An intuitionistic theory of types. In Giovanni Sambin and Jan M. Smith, edi- tors, Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 127–172. Oxford University Press, 1998.
matics, 30:222–262, 1908.
34:839–864, 1933.
[chu40]: Alonzo Church. A formulation of of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
[chu41]: Alonzo Church. The Calculi of Lambda Conversation. Princeton University Press, 1941.
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?