Introduction to higher-order logic (type theory) with primary emphasis on the typed lambda-calculus. Syntax and semantics, lambda-notation, axiomatic treatment, axioms of Descriptions, Choice, and Infinity, weak completeness, weak compactness, standard and non-standard models. Computer-assisted formal proofs. Formalization of mathematics, definability of natural numbers, representability of recursive functions, Church's Thesis. Godel's Incompleteness Theorems, undecidability, undefinability. Prerequisite: 21-600 or permission of instructor.