学术界里学生捧高老师也是很重要的。

简单类型论最早是Chwistek和Ramsey的工作，现在极少看到被提及。

Lesniewski是第一个提出现代意义上类型的人，他称之为Semantic Category，目前很确定的是早在1929年的Lecture里他就完成了他的三部曲系统并且大量使用这个标记。但是他本人没有形式化这个理论，形式化的工作是1935年左右他的同事做的。

Curry的关于Functionality组合子的论文最初发表在1934-1936年，连续几篇。

这些工作都早于Alonzo Church在1940年的简单类型论。而且简单类型论的重点并不是要形式化type，而是利用type表达高阶逻辑和禁止罗素悖论。

但是因为Church学派弟子三千，是北美理论计算机科学的半壁江山。学术史就成了学生们写的。[喵喵]