Abstract: The evolution of types and logic in the 20th century: A journey through Frege, Russell and other founders of modern logic and computation

Fairouz Kamareddine

The introduction of a general definition of function was key to Frege's formalisation of logic. Self-application of functions was at the heart of Russell's paradox. Russell introduced type theory in order to control the application of functions and hence to avoid the paradox. Since, different type systems have been introduced, each allowing different functional power. Despite the extensive use of types in many applications, there remains many ``non believers'' in type theory. In this talk, I will briefly review the evolution of types from the time of Euclid (325 B.C.) to the mid of the 20th century. Then, I will introduce de Bruijn's formulation of functions and types in Automath, his famous system for automating mathematics. De Bruijn's formulation is a living example which illustrates that while type theory is useful, there are many other considerations that need to be accommodated when attempting to ``computerize'' a system. This talk is of interest for anyone interested in the foundation and implementation of logic, mathematics, computer science and natural or programming language.