This is a learning seminar on dependent type theory. We are currently following Peter Selinger's lecture notes on the lambda calculus (available online here: https://www.mathstat.dal.ca/~selinger/papers/lambdanotes.pdf). This talk will cover part of chapter 6 (specifically sections 6.1, 6.6, and 6.7) and and chapter 7 of Selinger's notes, on the simply-typed lambda calculus and normalization, respectively. The talk may also incorporate material from chapters 4 and 6 of the textbook "Proofs and Types" by Girard, Lafont and Taylor (which cover normalization for the simply typed lambda calculus).