Introduction to Type Theory

Undergraduate / Graduate

Type theory is a new way of thinking about logic in which proofs are associated with computational verifications. It revolves around the Curry-Howard correspondence, which connects the idea of proof with the idea of computation. This class will introduce students both to the mathematical and philosophical issues involved in this way of looking at logic. In particular, the Curry-Howard correspondence will be examined in both simple and complex forms, culminating in versions of the Curry-Howard correspondence for classical logic that involve lambda calculi of catching and throwing exceptions, as well versions of the Curry-Howard correspondence for higher order logic that involve dependent type theory. This will all be used to give a novel account of the meaning of the logical connectives, as well as a different way of viewing the fundamental difference between intuitionistic and classical logic. The course will use notes from a forthcoming book, and students without knowledge of the lambda calculus are advised to contact the professor for some preparatory reading. The class is suitable for those who already have a working familiarity with the ideas of elementary logic. (B) (II)