Activity: Talk or presentation › Oral presentation
Description
Most modern mathematics relies on set theory to work - a comprehensively studied and well understood system relying on sets and set membership. However, it is not the only theory we can build mathematics from. Type theory, first proposed by Bertrand Russel and later studied and improved by figures such as Alonzo Church and Per Martin-Löf, is one such theory that has found its way into how we construct programming languages and verify mathematical proofs. In this talk, we introduce the basics of type theory and discuss both its history and the motivations for its modern uses.