报告题目: From the foundation of mathematics to the birth of computation
Abstract. Mathematics is old, Logic is old, but in some sense, many basic ideas of the foundation of computer science are old too. For example, that proof checking (or type checking) is decidable but proof construction (or type inference) is not, was hinted at by Aristotle. In this talk, I go through some of the developments in mathematics and logic which influenced the creation of some computer science ideas in the 20th century. In particular, I discuss how the need for more precision and formality in the 18th century, led to the development of logic in the 19th century, to the work of Frege and the discovery of Russell’s paradox. I then discuss the use of type theory (a concept that was already implicit in Euclid’s Geometry 325 B.C.) by Russell to avoid the paradox and explain the development and the influence of types in computation.