Type Theory

Undergraduate / Graduate

Church's λ-calculus, β-reduction, the Church-Rosser theorem. Simple type theory, strong normalization. The Barendregt cube of type theories. Dependent types. The Curry-Howard Isomorphism. Formal constructive mathematics.