An Introduction to Type Theory

Activity: Talk or presentationOral presentation


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.
Period28 Feb 2024
Held atDepartment of Mathematics
Degree of RecognitionLocal


  • type theory
  • logic
  • mathematics
  • paradox
  • lambda calculus
  • computer science